Leonardo de Moura a5d1b8f3c5 chore: add Macro.State		2021-04-23 16:22:24 -07:00
..
Control	chore: remove when and «unless»	2021-03-20 18:52:18 -07:00
Data	chore: #405 step 1	2021-04-22 20:03:48 -07:00
System	chore: remove leftovers	2021-03-23 17:33:23 -07:00
Classical.lean	refactor: cases	2021-03-07 12:37:02 -08:00
Coe.lean	feat: CoeSort Bool Prop	2021-03-20 14:52:16 +01:00
Control.lean	feat: add ExceptCpsT	2021-02-27 18:44:24 -08:00
Core.lean	refactor: clean up Thunk	2021-04-22 20:29:08 -07:00
Data.lean	feat: add Ord and deriving instance for it.	2021-04-03 21:27:26 -07:00
Fix.lean	refactor: arbitrary without explicit arguments	2020-11-25 09:07:38 -08:00
Hints.lean	fix: Not should not be reducible, special support for Ne	2021-02-15 17:36:11 -08:00
Meta.lean	chore: fix StructInst and add mkGroupNode	2021-04-07 22:46:07 -07:00
Notation.lean	chore: #405 step 1	2021-04-22 20:03:48 -07:00
NotationExtra.lean	feat: basic unexpanders for Exists & Sigma	2021-02-04 11:04:37 +01:00
Prelude.lean	chore: add Macro.State	2021-04-23 16:22:24 -07:00
SimpLemmas.lean	feat: add missing simp lemmas for <->	2021-04-05 06:41:39 -07:00
SizeOf.lean	chore: define SizeOf Lean.Name instance manually	2021-01-20 18:07:14 -08:00
System.lean	chore: remove #lang lean4 header	2020-10-25 09:54:07 -07:00
Util.lean	feat: add Prelude.lean	2020-11-10 18:08:18 -08:00
WF.lean	chore: remove unnecessary generalizing	2021-03-27 15:03:13 -07:00