max - Network

So if you have one type which uses mutual inductive types, induction-induction (II), induction-recursion (IR), and recursion-recursion (RR),...

So if you have one type which uses mutual inductive types, induction-induction (II), induction-recursion (IR), and recursion-recursion (RR), is that an... IIRRT? An IIIRRRT?
I may be cooking something very silly.

Exam season is over. Time for some cursed Lean experiments >:3. This is probably a very bad idea, but it is pretty cool that it is...

Exam season is over. Time for some cursed Lean experiments >:3. This is probably a very bad idea, but it is pretty cool that it is possible at all.

Unfortunately the lack of proper universe polymorphism makes this quite limited. You also can't name the `(x : A) -> ...` binders when you call `ForallTelescopeP`.

🤔

🤔

Why *not* copy-paste an SMT-generated Alethe2 proof directly into your Lean theorem, and let each step be elaborated as if it was a tactic,...

Why *not* copy-paste an SMT-generated Alethe2 proof directly into your Lean theorem, and let each step be elaborated as if it was a tactic, haha...
And you can watch exactly how the tactic state changes with each step, subproofs start and end, etc...

(Slowly trying to get proof reconstruction working for a lean hammer, this is still very hacky and uses a lot of shortcuts)