lean4-htt/src/Init
Leonardo de Moura b95c4788c1 refactor: OfDecimal ==> OfScientific
`decimalLit` ==> `scientificLit`
2020-12-03 08:08:19 -08:00
..
Control fix: <&> 2020-12-01 11:57:20 -08:00
Data refactor: OfDecimal ==> OfScientific 2020-12-03 08:08:19 -08:00
System chore: update structure, class, inductive 2020-11-27 15:09:30 -08:00
Classical.lean fix: ambiguity at induction/cases 2020-11-24 14:59:12 -08:00
Coe.lean feat: heterogeneous OrElse and AndThen 2020-12-01 18:32:24 -08:00
Control.lean chore: merge src/Control files 2020-11-10 18:47:23 -08:00
Core.lean chore: adjust stdlib 2020-11-29 17:01:56 -08:00
Data.lean refactor: OfDecimal ==> OfScientific 2020-12-03 08:08:19 -08:00
Fix.lean refactor: arbitrary without explicit arguments 2020-11-25 09:07:38 -08:00
Meta.lean refactor: OfDecimal ==> OfScientific 2020-12-03 08:08:19 -08:00
Notation.lean feat: heterogeneous OrElse and AndThen 2020-12-01 18:32:24 -08:00
NotationExtra.lean fix: notation 2020-11-29 08:28:01 -08:00
Prelude.lean refactor: OfDecimal ==> OfScientific 2020-12-03 08:08:19 -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: update structure, class, inductive 2020-11-27 15:09:30 -08:00