Leonardo de Moura 58c938cef8 feat: 'termination_by' goodies		2021-09-22 21:09:33 -07:00
..
Structural	fix: bug introduced today	2021-09-21 20:36:18 -07:00
WF	feat: 'termination_by' goodies	2021-09-22 21:09:33 -07:00
Basic.lean	chore: use doc string	2021-09-17 14:20:28 -07:00
Main.lean	feat: 'termination_by' goodies	2021-09-22 21:09:33 -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