lean4-htt/src/Init
2022-07-26 15:13:28 -07:00
..
Control chore: convert doc/mod comments from /- to /--//-! (#1354) 2022-07-22 12:05:31 -07:00
Data perf: avoid blowup at deriving Repr 2022-07-24 13:10:04 -07:00
System chore: convert doc/mod comments from /- to /--//-! (#1354) 2022-07-22 12:05:31 -07:00
Classical.lean refactor: remove some unnecessary antiquotation kind annotations 2022-07-23 17:09:32 +02:00
Coe.lean chore: convert doc/mod comments from /- to /--//-! (#1354) 2022-07-22 12:05:31 -07:00
Control.lean feat: add ExceptCpsT 2021-02-27 18:44:24 -08:00
Conv.lean refactor: remove some unnecessary antiquotation kind annotations 2022-07-23 17:09:32 +02:00
Core.lean chore: convert doc/mod comments from /- to /--//-! (#1354) 2022-07-22 12:05:31 -07:00
Data.lean refactor: move ac proofs to Init. 2022-03-16 17:21:20 -07:00
Hints.lean fix: Not should not be reducible, special support for Ne 2021-02-15 17:36:11 -08:00
Meta.lean refactor: remove some unnecessary antiquotation kind annotations 2022-07-23 17:09:32 +02:00
Notation.lean feat: add with_annotate_term 2022-07-26 15:13:28 -07:00
NotationExtra.lean feat: improve calc tactic 2022-07-24 14:30:15 -07:00
Prelude.lean chore: convert doc/mod comments from /- to /--//-! (#1354) 2022-07-22 12:05:31 -07:00
SimpLemmas.lean feat: boolean inequality lemmas 2022-06-25 11:18:09 +02:00
SizeOf.lean chore: convert doc/mod comments from /- to /--//-! (#1354) 2022-07-22 12:05:31 -07:00
SizeOfLemmas.lean feat: add helper sizeOf simp theorems 2022-02-28 12:28:37 -08:00
System.lean chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00
Tactics.lean refactor: remove some unnecessary antiquotation kind annotations 2022-07-23 17:09:32 +02:00
Util.lean chore: convert doc/mod comments from /- to /--//-! (#1354) 2022-07-22 12:05:31 -07:00
WF.lean chore: remove codegen option 2022-07-07 08:18:30 -07:00
WFTactics.lean refactor: remove some unnecessary antiquotation kind annotations 2022-07-23 17:09:32 +02:00