ea22ef4485
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. |
||
|---|---|---|
| .. | ||
| compiler | ||
| constructions | ||
| annotation.cpp | ||
| annotation.h | ||
| aux_recursors.cpp | ||
| aux_recursors.h | ||
| bin_app.cpp | ||
| bin_app.h | ||
| class.cpp | ||
| class.h | ||
| CMakeLists.txt | ||
| constants.cpp | ||
| constants.h | ||
| constants.txt | ||
| expr_lt.cpp | ||
| expr_lt.h | ||
| expr_pair.h | ||
| expr_pair_maps.h | ||
| expr_unsigned_map.h | ||
| formatter.cpp | ||
| formatter.h | ||
| init_module.cpp | ||
| init_module.h | ||
| max_sharing.cpp | ||
| max_sharing.h | ||
| module.cpp | ||
| module.h | ||
| num.cpp | ||
| num.h | ||
| print.cpp | ||
| print.h | ||
| profiling.cpp | ||
| profiling.h | ||
| projection.cpp | ||
| projection.h | ||
| reducible.cpp | ||
| reducible.h | ||
| replace_visitor.cpp | ||
| replace_visitor.h | ||
| suffixes.h | ||
| time_task.cpp | ||
| time_task.h | ||
| util.cpp | ||
| util.h | ||