lean4-htt/src/Init
2021-01-13 10:26:45 -08:00
..
Control refactor: Repr 2020-12-18 11:21:30 -08:00
Data feat: add Float.neg and casts 2021-01-13 10:26:45 -08:00
System fix: remove auto-cancellation of IO tasks 2020-12-30 17:03:09 +01:00
Classical.lean chore: use instance (priority := <prio>) 2020-12-21 10:17:54 -08:00
Coe.lean chore: cleanup and style 2020-12-12 10:36:26 -08:00
Control.lean chore: merge src/Control files 2020-11-10 18:47:23 -08:00
Core.lean feat: simpArrow 2021-01-01 17:15:15 -08:00
Data.lean feat: add helper classes for implementing parallel for 2020-12-19 14:15:47 -08:00
Fix.lean refactor: arbitrary without explicit arguments 2020-11-25 09:07:38 -08:00
Meta.lean feat: allow user to set Simp.Config at simp 2021-01-01 15:12:18 -08:00
Notation.lean feat: allow user to set Simp.Config at simp 2021-01-01 15:12:18 -08:00
NotationExtra.lean fix: sigma notation precedence 2020-12-26 09:35:40 -08:00
Prelude.lean feat: "implement" sorry using panic 2021-01-13 09:43:25 -08:00
SimpLemmas.lean feat: simpArrow 2021-01-01 17:15:15 -08:00
SizeOf.lean chore: update structure, class, inductive 2020-11-27 15:09:30 -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: cleanup and style 2020-12-12 10:36:26 -08:00