pnat and equation compiler?

Stream: general

[Kevin Buzzard]

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]

is it possible to build a custom equation compiler?

[Mario Carneiro]

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

[Mario Carneiro]

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