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

895 commits

Author SHA1 Message Date
Leonardo de Moura
6547af988b feat: add substVars 2022-01-25 18:43:51 -08:00
Leonardo de Moura
234f70fadb chore: remove the now incorrect comment 2022-01-24 19:05:05 -08:00
Leonardo de Moura
02677cf326 fix: igore instance implicit arguments in term ordering used at simp 
closes #972
 2022-01-24 18:57:31 -08:00
Leonardo de Moura
d4f7899591 chore: avoid code duplication setting Simp.Config 2022-01-24 18:57:31 -08:00
Leonardo de Moura
722bf54929 fix: trace message with incorrect MetavarContext 2022-01-24 10:34:44 -08:00
Leonardo de Moura
7ada79bf2e fix: use an AC-compatible ordering on Expr at simp 
closes #968
 2022-01-22 09:42:59 -08:00
Leonardo de Moura
6f416147b4 chore: rename coeM and liftCoeM 2022-01-20 15:33:17 -08:00
Leonardo de Moura
2192e6148b chore: remove coe, coeSort, and coeFun abbreviations 
The notation `↑ e` is now expanded eagerly.

See #403
 2022-01-20 15:19:06 -08:00
Leonardo de Moura
3c17755730 chore: prepare to remove coe definitions 
The notation `↑ e` will eagerly expand the coersion.

See #403
 2022-01-20 15:07:54 -08:00
Leonardo de Moura
d190d6dda4 fix: use default reducibility when proving equation theorems for definition 
Addresses issue reported by @fpfu at #945
 2022-01-20 08:23:51 -08:00
Leonardo de Moura
f5509ab867 fix: equational lemma generation for definitions using named patterns 
closes #945
 2022-01-19 17:45:54 -08:00
Leonardo de Moura
ef449e816f chore: improve trace messages 2022-01-19 14:29:04 -08:00
Leonardo de Moura
873a2ba8a6 feat: unfold namedPattern applications at equation theorems 2022-01-18 15:03:20 -08:00
Leonardo de Moura
1e21815e41 fix: equality theorem generation when named patterns are used 
closed #945
 2022-01-18 14:37:51 -08:00
Leonardo de Moura
c816524d8d feat: add subst? 2022-01-18 14:26:14 -08:00
Leonardo de Moura
c12fa6f0e2 fix: error message 
The equation theorems may fail for other reasons.
 2022-01-18 14:11:54 -08:00
Leonardo de Moura
1c1e6d79a7 feat: add equality proof for named patterns 
The user can optionally name the equality proof.
The new test demostrates how to name the equality proof.

closes #501
 2022-01-18 12:43:01 -08:00
Leonardo de Moura
42fe01a3eb feat: add new flag to caseValues 2022-01-18 12:15:29 -08:00
Leonardo de Moura
9d05023325 chore: remove some [specialize] annotations 2022-01-18 09:24:06 -08:00
Leonardo de Moura
6631f1d5b3 chore: use namedPatternOld 2022-01-17 17:18:03 -08:00
Leonardo de Moura
2c690926cf feat: update namedPattern parser 2022-01-17 16:49:20 -08:00
Leonardo de Moura
de11f7e1bc feat: add sizeOf spec lemmas as simp theorems 2022-01-17 16:14:38 -08:00
Leonardo de Moura
8f47043aee chore: add trace message for sizeOf theorem 2022-01-17 15:42:42 -08:00
Leonardo de Moura
bac91b9b5b chore: remove arbitrary 2022-01-15 12:14:27 -08:00
Leonardo de Moura
7d5f14b4a7 chore: elaborate default_or_ofNonempty% and add mkDefault 2022-01-15 11:55:58 -08:00
Leonardo de Moura
f1adedb2de feat: add Classical.ofNonempty 2022-01-14 15:59:11 -08:00
Leonardo de Moura
49b2860f2a feat: add Meta.rename tactic 2022-01-12 16:15:30 -08:00
Leonardo de Moura
7a86b613dc chore: remove old comment 2022-01-12 08:28:03 -08:00
Leonardo de Moura
b50e82bc93 feat: unfold tactic 2022-01-07 13:51:45 -08:00
Leonardo de Moura
c303bf6916 refactor: add helper methods for simp 2022-01-07 13:51:45 -08:00
Leonardo de Moura
bef161caf7 feat: add better support for discharging equation theorem hypotheses 2022-01-06 14:42:23 -08:00
Leonardo de Moura
df6095e580 fix: casesOnStuckLHS method 
It was not general enough.
 2022-01-06 13:54:17 -08:00
Leonardo de Moura
90b179bea9 fix: add equation theorems even if definition supports smart unfolding 
See new test.
 2022-01-06 13:53:03 -08:00
Leonardo de Moura
60934bf1d5 feat: add support for removing [simp] attribute from definitions with equational theorems 2022-01-05 16:57:59 -08:00
Leonardo de Moura
c2e52bd577 feat: use getEqnsFor? when applying [simp] at definitions 2022-01-05 15:59:39 -08:00
Leonardo de Moura
030e932db8 feat: use getEqnsFor? at simp 2022-01-05 11:28:24 -08:00
Mario Carneiro
7956a9bb15
chore: typos 2021-12-23 10:14:39 +01:00
Leonardo de Moura
be6bc67eb0 fix: ensure match-expressions compiled using if-then-else can be reduced with TransparencyMode.reducible 
closes #891
 2021-12-18 10:55:42 -08:00
Leonardo de Moura
b3d8766b09 chore: use doubleticks at WHNF.lean 2021-12-18 08:43:50 -08:00
Leonardo de Moura
b6fbdd8679 feat: add Meta.Context.canUnfold? 2021-12-18 08:25:56 -08:00
Leonardo de Moura
c954fc9ec7 fix: bug at simpLoop 2021-12-18 06:48:08 -08:00
Leonardo de Moura
81f7335269 fix: ensure motive is type correct at simpProj 2021-12-15 17:07:31 -08:00
Leonardo de Moura
0a81093db5 fix: bug at simpProj 
This bug was reported at https://github.com/dwrensha/lean4-maze/issues/1
 2021-12-15 17:07:00 -08:00
Leonardo de Moura
1c83ea9e40 fix: typo at hasUnusedArguments 
See comment at #815
 2021-12-14 06:50:34 -08:00
Leonardo de Moura
a3361e7d86 fix: missing universe assignments made during TC resolution 
closes #796
 2021-12-12 07:07:13 -08:00
Leonardo de Moura
68bd55af32 chore: fix codebase 2021-12-10 13:12:09 -08:00
Leonardo de Moura
96e0e1db98 fix: nontermination at simp [OfNat.ofNat] 
closes #788
 2021-12-10 12:29:33 -08:00
Leonardo de Moura
41040a81de fix: auxiliary matcher definitions should be treated as abbreviations 
The motivation is to prevent performance problems such as the one
described at issue #854.

Fixes #854 after a update stage0
 2021-12-07 16:43:20 -08:00
Leonardo de Moura
b0fe1e5d10 feat: add Tomas Skrivan's TC resolution improvement 
This commit implements the TC resolution improvement suggested by
Tomas at #815.

Closes #815.
 2021-12-06 17:46:11 -08:00
Leonardo de Moura
7b6732a137 refactor: ExprDefEq.lean and LevelDefEq.lean are now implementation only files 
We use the export/extern idiom to define `isLevelDefEqAux`, and then
define the `isDefEq` user facing functions at `Meta/Basic.lean`.
 2021-12-06 09:57:00 -08:00