max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Init
History
Floris van Doorn 32e93f1dc1
fix: delete Measure and SizeOfRef (#2275) 
* move Measure to Nat namespace

We could (and maybe should) also move various other declarations to namespaces, like measure. However, measure seems to be used a lot in termination_by statements, so that requires other fixes as well. Measure seems to be almost unused

* fix

* delete Measure and SizeOfRef instead
2023-06-21 22:51:28 -07:00
..
Control chore: add semiOutParam annotations 2023-04-10 13:00:04 -07:00
Data chore: remove intermediate 2023-06-05 15:50:11 -07:00
System fix: ignore vanishing files during watchdog update 2023-03-10 19:13:24 +01:00
Classical.lean fix: spacing in by_cases 2022-11-16 08:16:42 -08:00
Coe.lean doc: improve documentation of Init.Coe 2023-06-05 15:52:25 -07:00
Control.lean
Conv.lean fix: spacing and indentation fixes 2023-05-28 18:48:36 -07:00
Core.lean feat: remove partial in Init.Data.String.Basic 2023-06-05 15:50:11 -07:00
Data.lean feat: Channel 2022-09-05 08:52:46 -07:00
Dynamic.lean chore: snake-case attributes (part 2) 2022-10-19 09:28:08 -07:00
Hints.lean
Meta.lean feat: hygieneInfo parser (aka this 2.0) 2023-06-02 16:19:02 +02:00
Notation.lean feat: implement have this (part 1) 2023-06-02 16:19:02 +02:00
NotationExtra.lean fix: spacing around calc 2023-06-02 09:15:15 +02:00
Prelude.lean feat: hygieneInfo parser (aka this 2.0) 2023-06-02 16:19:02 +02:00
ShareCommon.lean chore: snake-case attributes (part 2) 2022-10-19 09:28:08 -07:00
SimpLemmas.lean chore: add missing simp lemma (¬ False) = True 2023-04-10 21:05:54 -07:00
SizeOf.lean doc: documentation for Init.SizeOf 2022-08-17 14:48:10 -07:00
SizeOfLemmas.lean feat: add helper sizeOf simp theorems 2022-02-28 12:28:37 -08:00
System.lean feat: Mutex, Condvar 2022-09-05 08:52:46 -07:00
Tactics.lean feat: implement have this (part 1) 2023-06-02 16:19:02 +02:00
Util.lean chore: snake-case attributes (part 2) 2022-10-19 09:28:08 -07:00
WF.lean fix: delete Measure and SizeOfRef (#2275) 2023-06-21 22:51:28 -07:00
WFTactics.lean fix: add done alternative to decreasing_with (#2019) 2023-01-09 09:46:37 -08:00