max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
32284 commits 1 branch 0 tags 5.3 GiB
Commit graph

46 commits

Author SHA1 Message Date
Scott Morrison
9cea1a503e
chore: upstream Std.Data.Prod.Lex (#3338) 2024-02-15 02:47:08 +00:00
Junyan Xu
2aeeed13cf
fix: generalize Prod.lexAccessible to match Lean 3 (#2388) 
* fix: generalize Prod.lexAccessible to match Lean 3

* fix

* fix
 2023-08-09 08:54:53 -07:00
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
Scott Morrison
1b50292228 chore: protect Prod.Lex 2022-11-29 20:09:08 +01:00
Adrien Champion
33aa1724f2 fix: rewrite by with strict indentation in a few struct-fields 2022-11-08 08:30:42 -08:00
Leonardo de Moura
eafd2a88ce chore: simplify Prelude.lean and Core.lean using elabAsElim 2022-07-29 18:13:56 -07:00
Leonardo de Moura
dd924e5270 chore: remove codegen option 
We should use `noncomputable` modifier instead.

closes #1288
 2022-07-07 08:18:30 -07:00
Wojciech Nawrocki
2a53857928 feat: add strong Nat induction principle 2022-06-12 14:01:05 -07:00
Leonardo de Moura
c2ddebc193 chore: unused variables 2022-06-07 16:47:04 -07:00
Sebastian Ullrich
ae7b895f7a refactor: unname some unused variables 2022-06-07 16:37:45 -07:00
Leonardo de Moura
619186b2a8 feat: only use set_option codegen false where needed 2022-03-06 19:15:05 -08:00
Leonardo de Moura
3005bab970 feat: helper theorem and tactic for WF 2022-02-28 15:11:00 -08:00
Leonardo de Moura
2ba3205f94 feat: add Prod.Lex.right' 2022-02-28 11:19:28 -08:00
Leonardo de Moura
3fbf5acbee fix: add missing [reducible] annotations Init/WF.lean 2022-01-12 17:12:55 -08:00
Leonardo de Moura
1a6abe1dad feat: WellFoundedRelation as a class 2022-01-12 08:28:03 -08:00
Leonardo de Moura
ec49c31337 chore: make sure PSigma.lex signature is similar to Prod.lex 2022-01-11 14:37:53 -08:00
Leonardo de Moura
4c051896df refactor: sizeofMeasure => sizeOfWFRel 
This commit also makes the first argument of `sizeOfWFRel` implicit.
 2021-09-27 19:06:10 -07:00
Leonardo de Moura
d4509878bb feat: add WellFoundedRelation for termination_by 2021-09-25 17:21:03 -07:00
Leonardo de Moura
bb98057098 refactor: avoid wf suffix 2021-09-21 12:57:08 -07:00
Leonardo de Moura
10a38aef3c chore: remove class WellFoundedRelation 
It is dead code.
 2021-09-21 12:57:08 -07:00
Leonardo de Moura
9bb5d4dc93 chore: Nat.ltWf => Nat.lt_wf 2021-09-02 07:51:41 -07:00
Leonardo de Moura
a821dcbff2 chore: enforce naming convention for theorems 
see issue #402

fix: `ElabTerm.lean`
 2021-08-07 12:48:38 -07:00
Leonardo de Moura
f4a7ffd8c8 chore: fix codebase and tests 2021-06-29 17:14:52 -07:00
Sebastian Ullrich
a02c6fd3eb chore: adapt stdlib & tests 2021-05-20 15:17:36 -07:00
Leonardo de Moura
08d865b475 chore: remove unnecessary generalizing 2021-03-27 15:03:13 -07:00
Leonardo de Moura
fba719ff02 chore: adjust WF.lean 2021-02-01 18:08:48 -08:00
Sebastian Ullrich
0c91b3769e chore: replace variables in src/ 2021-01-22 14:36:05 +01:00
Leonardo de Moura
5249fdc24d chore: cleanup and style 2020-12-12 10:36:26 -08:00
Leonardo de Moura
0869f38de4 chore: update structure, class, inductive 2020-11-27 15:09:30 -08:00
Leonardo de Moura
b72a3c69b6 fix: ambiguity at induction/cases 
See efc3a320fe
 2020-11-24 14:59:12 -08:00
Leonardo de Moura
304c80d610 feat: use <| 2020-11-19 09:03:38 -08:00
Leonardo de Moura
c305c2691f chore: use := 2020-11-19 07:22:31 -08:00
Leonardo de Moura
7e51020685 chore: move SizeOf to its own file 2020-11-10 14:43:03 -08:00
Leonardo de Moura
bf4d48f348 chore: cleanup for presentation 2020-11-05 12:43:02 -08:00
Leonardo de Moura
a6fd611db0 chore: use generalizing 2020-11-02 17:01:10 -08:00
Leonardo de Moura
a0ab1b9eb4 chore: remove with 2020-11-02 13:35:26 -08:00
Leonardo de Moura
dfc346e76f chore: remove obsolete attribute 2020-11-02 06:47:20 -08:00
Leonardo de Moura
6858cb5fb6 chore: cleanup 2020-10-29 10:24:16 -07:00
Leonardo de Moura
898a08a0c1 chore: avoid Has prefix in type classes 
closes #203
 2020-10-27 18:29:19 -07:00
Leonardo de Moura
97c93ec557 chore: prepare to rename 2020-10-27 18:09:03 -07:00
Leonardo de Moura
13c2a8ff51 chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00
Leonardo de Moura
535765993a chore: move to new frontend 2020-10-23 19:59:46 -07:00
Leonardo de Moura
50990b99d6 chore: remove unnecessary annotations 2020-05-12 15:02:03 -07:00
Leonardo de Moura
33a10130cf chore: fix stdlib 2020-05-12 15:02:03 -07:00
Leonardo de Moura
1784b0ee67 chore: Heq ==> HEq 2019-12-04 11:20:38 -08:00
Leonardo de Moura
c445199747 chore: library/Init ==> src/Init 
cc @Kha @dselsam @cipher1024
 2019-11-22 06:06:05 -08:00
Renamed from library/Init/WF.lean (Browse further)