Zulip Chat Archive

Stream: general

Topic: pnat and equation compiler?


Kevin Buzzard (Nov 16 2018 at 22:23):

Can I somehow make the equation compiler work on pnat as well as it works on nat? Something like

def f : ℕ+  ℕ+
| 1 := 37
| (n + 1) := 2 * f n

How does the equation compiler work? It is presumably bound to the inbuilt constructors? Would this basically just entail writing a new pnat with one and succ and then defining stuff like * on the new structure?

Kenny Lau (Nov 16 2018 at 22:26):

is it possible to build a custom equation compiler?

Mario Carneiro (Nov 16 2018 at 22:32):

right. Lean 3 doesn't have the necessary customizability for this

Mario Carneiro (Nov 16 2018 at 22:33):

Although we could write our own equation compiler if we write our own version of def


Last updated: Dec 20 2023 at 11:08 UTC