lean4-htt/src/Init
2020-11-20 15:47:27 -08:00
..
Control chore: remove some unnecessary commas 2020-11-20 15:47:27 -08:00
Data feat: add support for unbound implicit locals 2020-11-20 12:22:27 -08:00
System feat: add helper instance 2020-11-19 11:32:54 -08:00
Classical.lean feat: use <| 2020-11-19 09:03:38 -08:00
Coe.lean feat: use <| 2020-11-19 09:03:38 -08:00
Control.lean chore: merge src/Control files 2020-11-10 18:47:23 -08:00
Core.lean feat: use <| 2020-11-19 09:03:38 -08:00
Data.lean refactor: rename LeanInit ==> Meta, and reduce dependencies 2020-11-13 16:00:31 -08:00
Fix.lean fix: UInt* and USize Inhabited instances 2020-11-13 16:30:48 -08:00
Meta.lean feat: use <| 2020-11-19 09:03:38 -08:00
Notation.lean feat: define $ notation at Notation.lean 2020-11-19 09:10:19 -08:00
NotationExtra.lean feat: define tactic parsers using syntax command 2020-11-17 13:52:36 -08:00
Prelude.lean chore: remove some unnecessary commas 2020-11-20 15:47:27 -08:00
SizeOf.lean chore: move SizeOf to its own file 2020-11-10 14:43:03 -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 feat: use <| 2020-11-19 09:03:38 -08:00