lean4-htt/src/Init
2021-08-13 16:26:35 -07:00
..
Control feat: add Alternative (StateRefT' ω σ m) 2021-08-10 14:27:05 -07:00
Data chore: change Pow class 2021-08-12 13:59:55 -07:00
System chore: enforce naming convention for theorems 2021-08-07 12:48:38 -07:00
Classical.lean chore: enforce naming convention for theorems 2021-08-07 12:48:38 -07:00
Coe.lean chore: fix codebase and tests 2021-06-29 17:14:52 -07:00
Control.lean feat: add ExceptCpsT 2021-02-27 18:44:24 -08:00
Core.lean fix: protect rfl 2021-08-07 13:25:54 -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: enforce naming convention for theorems 2021-08-07 12:48:38 -07:00
Notation.lean chore: use binop% to define ++ notation 2021-08-13 16:26:35 -07:00
NotationExtra.lean feat: unexpander for Subtype 2021-08-12 09:32:33 +02:00
Prelude.lean chore: change Pow class 2021-08-12 13:59:55 -07:00
SimpLemmas.lean chore: remove staging workaround theorems 2021-08-07 12:52:31 -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 chore: enforce naming convention for theorems 2021-08-07 12:48:38 -07:00
WF.lean chore: enforce naming convention for theorems 2021-08-07 12:48:38 -07:00