Leonardo de Moura 988e43d2b4 fix: WF should reject definitions that do not take any arguments		2021-10-04 13:24:30 -07:00
..
Structural	chore: style	2021-09-26 15:52:13 -07:00
WF	fix: WF should reject definitions that do not take any arguments	2021-10-04 13:24:30 -07:00
Basic.lean	chore: use doc string	2021-09-17 14:20:28 -07: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