lean4-htt/src/Init
2021-03-11 08:06:20 -08:00
..
Control chore: add annotations 2021-03-10 14:11:03 -08:00
Data chore: remove old decide!, nativeRefl!, and nativeDecide! 2021-03-11 08:06:20 -08:00
System fix: go-to-def paths on Windows 2021-01-28 11:45:33 -08:00
Classical.lean refactor: cases 2021-03-07 12:37:02 -08:00
Coe.lean chore: remove nested outParam 2021-01-29 17:13:03 -08:00
Control.lean feat: add ExceptCpsT 2021-02-27 18:44:24 -08:00
Core.lean chore: fix Core.lean 2021-03-07 12:08:37 -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
Hints.lean fix: Not should not be reducible, special support for Ne 2021-02-15 17:36:11 -08:00
Meta.lean refactor: move ToString Syntax and BEq Syntax to Init 2021-02-26 13:21:04 -08:00
Notation.lean chore: remove old decide!, nativeRefl!, and nativeDecide! 2021-03-11 08:06:20 -08:00
NotationExtra.lean feat: basic unexpanders for Exists & Sigma 2021-02-04 11:04:37 +01:00
Prelude.lean chore: remove old decide!, nativeRefl!, and nativeDecide! 2021-03-11 08:06:20 -08:00
SimpLemmas.lean chore: annotations for simp 2021-02-15 17:04:47 -08: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: adjust WF.lean 2021-02-01 18:08:48 -08:00