This ports the `.below` and `.brecOn` constructions to lean.
I kept them in the same file, as they were in the C code, because they
are
highly coupled and the constructions are very analogous.
For validation I developed this in a separate repository at
https://github.com/nomeata/lean-constructions/tree/fad715e
and checked that all declarations found in Lean and Mathlib are
equivalent, up to
def canon (e : Expr) : CoreM Expr := do
Core.transform (← Core.betaReduce e) (pre := fun
| .const n ls => return .done (.const n (ls.map (·.normalize)))
| .sort l => return .done (.sort l.normalize)
| _ => return .continue)
It was not feasible to make them completely equal, because the kernel's
type inference code seem to optimize level expressions a bit less
aggressively, and beta-reduces less in inference.
The private helper functions about `PProd` can later move into their own
file, used by these constructions as well as the structural recursion
module.
ea22ef4485