lean4-htt/src/Init
2021-05-21 17:13:33 -07:00
..
Control chore: adapt stdlib & tests 2021-05-20 15:17:36 -07:00
Data chore: adapt stdlib & tests 2021-05-20 15:17:36 -07:00
System chore: remove leftovers 2021-03-23 17:33:23 -07:00
Classical.lean chore: adapt stdlib & tests 2021-05-20 15:17:36 -07: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 chore: adapt stdlib & tests 2021-05-20 15:17:36 -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: adapt stdlib & tests 2021-05-20 15:17:36 -07:00
Notation.lean feat: move block tactic macro to Init 2021-05-21 17:13:33 -07:00
NotationExtra.lean feat: class abbrev now supports a type spec (+ test) 2021-05-20 15:23:30 -07:00
Prelude.lean chore: adapt stdlib & tests 2021-05-20 15:17:36 -07:00
SimpLemmas.lean chore: adapt stdlib & tests 2021-05-20 15:17:36 -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: adapt stdlib & tests 2021-05-20 15:17:36 -07:00