lean4-htt/src/Lean/Elab/PreDefinition
2022-01-10 12:57:51 +01:00
..
Structural feat: add mkUnfoldEq skeleton 2022-01-06 17:42:45 -08:00
WF feat: add mkUnfoldEq skeleton 2022-01-06 17:42:45 -08:00
Basic.lean fix: apply afterCompilation attributes after we have compiled *all* definitions in a mutual block 2022-01-05 15:57:51 -08:00
Eqns.lean fix: clear local context at mkUnfoldEq 2022-01-07 13:51:45 -08:00
Main.lean feat: apply termination tactic provided by user 2021-10-03 18:47:52 -07:00
MkInhabitant.lean chore: style 2021-06-21 10:17:26 -07:00
Structural.lean refactor: split Structural.lean into smaller files 2021-09-11 03:40:51 -07:00
WF.lean refactor: add src/Lean/Elab/PreDefinition/WF directory 2021-09-21 15:44:21 -07:00