Leonardo de Moura
8bbe6cac02
chore: fix test
2021-05-17 14:47:24 -07:00
Leonardo de Moura
53b2ceea51
fix: missing withoutModifyingState at elabSimpConfig
2021-05-16 13:07:13 -07:00
Leonardo de Moura
ac90052139
feat: add option for controlling how deep we go when trying to discharge simp theorem hypotheses
2021-05-16 12:32:05 -07:00
Leonardo de Moura
a498a64490
chore: disable injectivity theorems generation for big structure tests
...
The test was producing a stack overflow in debug mode in CI.
2021-05-15 21:30:40 -07:00
Leonardo de Moura
5d305faee0
chore: increase threshold for Windows workaround in the previous commit
2021-05-15 21:15:37 -07:00
Leonardo de Moura
3b8b46b16c
test: closes #441
2021-05-15 20:37:48 -07:00
Leonardo de Moura
c7096f54a2
feat: injectivity theorems for types defined in the prelude
2021-05-14 18:32:26 -07:00
Leonardo de Moura
ea45d3bd40
fix: fixes #457
2021-05-12 20:45:54 -07:00
Leonardo de Moura
4db3ccaddb
feat: type ascription should disable implicit lambdas
2021-05-12 19:29:36 -07:00
Leonardo de Moura
b52edf1259
fix: fixes #452
...
The new syntax is similar to `matchAlts` and uses `colGe`.
The first `|` is not optional anymore.
2021-05-10 17:28:10 -07:00
Leonardo de Moura
4675817a9e
fix: projection of string literals
2021-05-07 14:38:21 -07:00
Leonardo de Moura
5fcd08326f
fix: bug at reduceRec
2021-05-07 14:21:37 -07:00
Leonardo de Moura
7fc6607611
feat: have ... := ... syntax closer to let
2021-05-06 15:38:57 -07:00
Sebastian Ullrich
e6132d37a5
fix: induction/cases: accept wildcard alternative even if some (but not all) cases have been excluded
2021-05-06 14:28:00 +02:00
Leonardo de Moura
164b26bf01
fix: make sure the resulting array size is equal to the number of binders
...
The following code relies on this property
```lean
for uid in scope.varUIds, x in xs do
sectionFVars := sectionFVars.insert uid x
```
2021-05-04 19:46:14 -07:00
Leonardo de Moura
56d5d6c564
chore: fix tests
2021-05-04 15:42:03 -07:00
Leonardo de Moura
1a0fc816b1
feat: rename inaccessible variable names at cases
2021-05-01 21:51:58 -07:00
Leonardo de Moura
a2e8bc0780
feat: use binop% to define arith operators
...
closes #382
2021-04-30 19:40:45 -07:00
Leonardo de Moura
adae6fdb40
fix: tolerate type incorrect terms
...
This bug was producing a type error when I was using `set_option trace.Elab true`
2021-04-29 21:34:15 -07:00
Leonardo de Moura
18085b9712
fix: improve match generalizing feature
2021-04-26 19:22:03 -07:00
Daniel Fabian
1f05f5bf11
chore: rename ProofBelow to below.
2021-04-26 20:33:21 +02:00
Leonardo de Moura
af391fe812
test: reflective inductive predicate
2021-04-25 20:35:13 -07:00
Daniel Fabian
eda4bdd337
test: extend inductive_pred.lean with tests using the new construction.
2021-04-25 20:02:22 -07:00
Leonardo de Moura
a6888f72dd
fix: instance + where + implicts issue
...
The following could not be elaborated.
```lean
instance : MulComm Bool where
mulComm := fun {a b} =>
match a, b with
| true, true => rfl
| true, false => rfl
| false, true => rfl
| false, false => rfl
```
2021-04-24 20:07:35 -07:00
Leonardo de Moura
74d613ab88
fix: safe instance for MethodsRef
2021-04-24 07:24:08 -07:00
Leonardo de Moura
964fd3f520
chore: fixes tests
...
closes #405
2021-04-22 20:22:43 -07:00
Leonardo de Moura
09d438ca1d
chore: enforce notation parameter naming convention
2021-04-19 18:54:09 -07:00
Leonardo de Moura
762cebbbfc
fix: match generalization bug
2021-04-19 18:37:25 -07:00
Leonardo de Moura
157ef80c5a
feat: match auto generalization
2021-04-16 21:48:38 -07:00
Leonardo de Moura
c1f45ecd48
fix: fixes #394
...
The bug was due to the auto-generalization feature.
2021-04-13 19:14:57 -07:00
Leonardo de Moura
adda3a9e02
fix: improve structural recursion
2021-04-13 10:31:43 -07:00
Leonardo de Moura
bf4b9b0ccd
fix: use noImplicitLambda% when defining tactic macros such as have, let, etc
...
Thus, we don't change the expected type when using them.
2021-04-12 23:01:47 -07:00
Leonardo de Moura
2f37d7e290
feat: elaborate noImplicitLambda% notation
2021-04-12 22:55:17 -07:00
Daniel Selsam
d35091da56
feat: parser alias for 'declVal'
2021-04-12 16:59:54 -07:00
Leonardo de Moura
217c0391bb
chore: example
2021-04-12 16:56:10 -07:00
Leonardo de Moura
565ca259b1
fix: issue raised by Andrew
2021-04-12 10:51:44 -07:00
Leonardo de Moura
6dbf227cf2
fix: issues #387 part 2
...
see #387
2021-04-10 15:51:07 -07:00
Leonardo de Moura
a2522fd316
test: for issue #387
...
closes #387
2021-04-10 15:15:19 -07:00
Leonardo de Moura
6d361b91b5
Feat: Add getAllParentStructures
2021-04-07 18:06:10 -07:00
Leonardo de Moura
e6dec2dd79
feat: don't allow whitespaces between . and field name
2021-04-05 07:11:14 -07:00
Daniel Fabian
401765f587
test: add test that deriving Ord compiles in various cases.
2021-04-03 21:27:26 -07:00
Leonardo de Moura
f631bd8df9
test: inductive predicate example
2021-04-02 16:21:54 -07:00
Sebastian Ullrich
ee55ac5508
chore: fix test
2021-03-31 21:24:28 +02:00
Leonardo de Moura
4ec6804667
fix: issue at expandMatchAlts
2021-03-30 12:55:59 -07:00
Leonardo de Moura
19e0a84817
fix: make the match behavior more uniform
2021-03-30 12:19:31 -07:00
Leonardo de Moura
b32b542a85
chore: fix mkForbiddenSet
2021-03-27 14:59:05 -07:00
Leonardo de Moura
4a0f8bf21a
feat: improve generalizing at induction
2021-03-27 14:28:03 -07:00
Leonardo de Moura
a8d672f237
test: add Kevin and Yakov's examples
2021-03-25 17:22:14 -07:00
Sebastian Ullrich
96c8cdfb14
chore: revert test changes
2021-03-25 10:35:22 +01:00
Leonardo de Moura
3176be136c
feat: improve "discriminant refinement"
2021-03-24 21:05:08 -07:00
