Leonardo de Moura c486203481 fix: use simpTargetStar when proving equation theorems for recursive definitions ... Add `take` function reported at Zulip.		2022-02-08 11:43:45 -08:00
..
Structural	fix: use simpTargetStar when proving equation theorems for recursive definitions	2022-02-08 11:43:45 -08:00
WF	fix: use simpTargetStar when proving equation theorems for recursive definitions	2022-02-08 11:43:45 -08:00
Basic.lean	chore: style	2022-02-06 07:29:26 -08:00
Eqns.lean	fix: use private names for theorems that are created on demand	2022-02-07 13:16:22 -08:00
Main.lean	chore: fix codebase after removing auto pure	2022-02-03 18:08:14 -08:00
MkInhabitant.lean	chore: elaborate default_or_ofNonempty% and add mkDefault	2022-01-15 11:55:58 -08: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