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

3447 commits

Author SHA1 Message Date
Leonardo de Moura
4f45a514fc fix: TC issue introduced by recent bug fix 
This commit fixes the issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/instance.20not.20synthesizing.20issue.3F
 2021-08-23 17:32:19 -07:00
Leonardo de Moura
79e6732fc6 fix: update tokenTable at withNamespace parser combinator 
It also moves `withOpen` and `withOpenDecl` applications to simplify
their definitions and make sure we do not need to reset the cache.
 2021-08-23 09:41:36 -07:00
Leonardo de Moura
7edc42fdfc fix: scoped command after open command 
The issue was reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Ending.20a.20command
 2021-08-23 08:29:30 -07:00
Leonardo de Moura
ca747e9b27 feat: use contradiction at leaves 
closes #644
 2021-08-22 18:41:02 -07:00
Leonardo de Moura
48e6188e89 feat: use exfalso at ElimEmptyInductive 2021-08-22 18:16:14 -07:00
Leonardo de Moura
7385cbfe2d test: add mapTR test 2021-08-22 16:51:38 -07:00
Leonardo de Moura
21c68a49e3 feat: elaborate nonrec modifier 2021-08-21 17:02:54 -07:00
Leonardo de Moura
46a5f06121 feat: do not consider dot notation when isAuxDecl is true 2021-08-21 16:35:32 -07:00
Leonardo de Moura
4d1d06fcbc chore: fix test 2021-08-21 15:07:36 -07:00
Leonardo de Moura
7066619123 refactor: define Nat.le using inductive type 2021-08-20 19:39:45 -07:00
Leonardo de Moura
7c9158a50e fix: structure command diamond support 
Fixes issue described at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Structure.20diamond.20error
 2021-08-19 07:45:21 -07:00
Leonardo de Moura
107712f8be feat: add instance from CoeSort to CoeTail 2021-08-18 20:24:43 -07:00
Leonardo de Moura
99e8a98f06 feat: allow universes metavariables from any depth to be assigned when ignoreLevelDepth is true 
We set `ignoreLevelDepth` to true during type class resolution.
 2021-08-18 20:20:51 -07:00
Leonardo de Moura
a5b9306e04 fix: deep recursion at contradiction 2021-08-17 21:32:32 -07:00
Leonardo de Moura
52b52b22ef fix: to do unfold matcher applications that cannot be reduced when smartUnfolding is true 
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/How.20to.20WHNF.20without.20exposing.20recursors.3F
 2021-08-17 21:32:32 -07:00
Leonardo de Moura
4fe65f3200 test: mathport issue https://github.com/dselsam/mathport/issues/18 2021-08-15 08:11:20 -07:00
Leonardo de Moura
9182ebd4c1 feat: elaborate * simp argument 2021-08-15 08:02:21 -07:00
Leonardo de Moura
3c68703f39 feat: elaborate <- modifier at simp arguments 2021-08-15 07:07:58 -07:00
Sebastian Ullrich
20accf5105 feat: revise macro parameter syntax 2021-08-12 07:48:42 -07:00
Leonardo de Moura
c68882ca67 feat: structure instance notation with multiple sources 
closes #462
closes #463
 2021-08-12 06:18:47 -07:00
Daniel Selsam
5952a857cd feat: pp.analyze improve heuristics for fun binders 2021-08-12 09:37:57 +02:00
Leonardo de Moura
f1738ce2a0 feat: add macro for expanding field abbrev notation 
The new macro allows us to use the field abbrev notation in patterns
too. See new test.
 2021-08-11 16:02:50 -07:00
Leonardo de Moura
61b3e6bcb8 fix: reduce projections of expanded structures at copyDefaultValue? 2021-08-10 20:50:59 -07:00
Leonardo de Moura
0623bb3860 feat: update fieldMap with composite field 2021-08-10 20:04:41 -07:00
Leonardo de Moura
ae03f15c92 test: default value set at copied structure 2021-08-10 19:00:34 -07:00
Leonardo de Moura
3b1285bee8 feat: process overriden default values in copied parents 2021-08-10 18:55:12 -07:00
Leonardo de Moura
295cae8afd feat: copy field default values 
Only basic examples are working. We still have many TODOs
 2021-08-10 16:53:10 -07:00
Leonardo de Moura
972f00b0ff fix: pending metavariable issue 
It fixes issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/let.20overload
 2021-08-10 14:52:53 -07:00
Leonardo de Moura
bc26a9b527 feat: improve copyNewFieldsFrom 2021-08-10 09:08:35 -07:00
Leonardo de Moura
9e5998baf0 feat: register instance/reducible attribute for structuer diamond coercions 2021-08-10 07:16:59 -07:00
Leonardo de Moura
a0bd964255 test: overriding default value of private field 2021-08-09 19:01:08 -07:00
Leonardo de Moura
3f3e5d9dcb fix: private field + default value bug 2021-08-09 19:01:08 -07:00
Daniel Selsam
0118c47117 refactor: separate pp.funBinderTypes and pp.piBinderTypes 2021-08-09 16:13:40 +02:00
Leonardo de Moura
1d9d8c7e75 chore: fix tests 
close #402
 2021-08-07 13:22:58 -07:00
Leonardo de Moura
a863f1b8a3 fix: fixes #616 2021-08-07 07:29:54 -07:00
Leonardo de Moura
8acbb55632 chore: fix tests 2021-08-06 14:05:00 -07:00
Leonardo de Moura
76cc99179d fix: fixes #370 2021-08-06 12:52:23 -07:00
Daniel Selsam
34a27f2d56 fix: pp.analyze strict implicits 2021-08-06 17:02:00 +02:00
Leonardo de Moura
bcfc927799 fix: fixes #602 2021-08-05 16:14:04 -07:00
Leonardo de Moura
4dbb3e6db1 fix: add workaround to prevent code explosion at deriving for FromJson 
fixes #569
 2021-08-05 06:58:07 -07:00
Wojciech Nawrocki
1b44768697 chore: fix test 2021-08-05 06:27:57 -07:00
Wojciech Nawrocki
3bbf19a404 feat: FromToJson for nested inductives 2021-08-05 06:27:57 -07:00
Leonardo de Moura
72e7bf4999 fix: synthPending bug 2021-08-04 20:07:06 -07:00
Daniel Selsam
d56db0a22d doc: pp.analyze one more comment about a failure 2021-08-03 09:13:18 +02:00
Daniel Selsam
2afc18323d doc: pp.analyze a few comments about failures 2021-08-03 09:13:18 +02:00
Daniel Selsam
d6253e091b fix: pp.analyze _s when forced explicit 2021-08-03 09:13:18 +02:00
Daniel Selsam
ea6fca24c2 refactor: pp.analyze StateT for analyzeApp 2021-08-03 09:13:18 +02:00
Daniel Selsam
aefd31b2a2 feat: better bottom-up/structure-type heuristics 2021-08-03 09:13:18 +02:00
Daniel Selsam
4c41142a61 chore: pp.analyze new test cases 2021-08-03 09:13:18 +02:00
Daniel Selsam
8dd8aea9c1 chore: new tests 2021-08-03 09:13:18 +02:00