Leonardo de Moura
34d8ecc066
fix: use show .. from .. to implement calc
...
Recall that `show .. from ..` ensures that proof has exactly the type
provided by the user.
In the new test, `rw [ih]` without this change because the goal would
be
```
... |- 0 + succ n = succ n
```
2021-08-29 11:33:50 -07:00
Leonardo de Moura
1f37cc7b41
feat: add next x₁ ... xₙ => tac tactic
2021-08-29 10:51:01 -07:00
Leonardo de Moura
1e5a4729c3
feat: case _ ... => ... as solve next goal
2021-08-29 10:45:38 -07:00
Leonardo de Moura
091efbec4f
test: simulate split tactic for match
2021-08-29 10:21:52 -07:00
Leonardo de Moura
9d5f211c28
feat: add environment extension for storing match conditional equations and splitter
2021-08-28 14:49:20 -07:00
Leonardo de Moura
e0e3de5c62
feat: allow (decidable) propositions at #eval
2021-08-27 15:06:48 -07:00
Leonardo de Moura
6713d8777a
fix: work duplication bug at specialize.cpp
...
closes #646
2021-08-27 10:35:27 -07:00
Leonardo de Moura
c897f63dd0
fix: using incorrect local context to process simp arguments
2021-08-26 12:49:12 -07:00
Leonardo de Moura
b5a434d8a9
test: for induction q with Quot.ind issue
...
See
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Induction.20alternative.20name.20when.20using.20Quot.2Eind.3F
2021-08-26 11:15:14 -07:00
Leonardo de Moura
1ede4843e3
feat: add renameI tactic
2021-08-25 18:50:59 -07:00
Leonardo de Moura
5003c74191
chore: fix test
2021-08-25 07:00:25 -07:00
Leonardo de Moura
42f1e16f44
chore: fix calc test
2021-08-25 06:59:46 -07:00
Sebastian Ullrich
f9fd0b3de4
feat: calc
2021-08-25 06:57:09 -07:00
Leonardo de Moura
214f2f7bb6
fix: toFVarsRHSArgs
2021-08-24 16:50:03 -07:00
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
