Leonardo de Moura 108518aad1 feat: use simp at mkDecreasingProof		2021-09-26 16:32:48 -07:00
..
Structural	chore: style	2021-09-26 15:52:13 -07:00
WF	feat: use simp at mkDecreasingProof	2021-09-26 16:32:48 -07:00
Basic.lean	chore: use doc string	2021-09-17 14:20:28 -07:00
Main.lean	feat: elaborate temination_by term	2021-09-25 16:54:41 -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