Leonardo de Moura
d380808930
fix: generalize if target is a let-declaration
2022-04-06 11:08:41 -07:00
Leonardo de Moura
eae4b92b0d
feat: use sorry if failed to synthesize default element for unsafe constant
2022-04-05 16:52:54 -07:00
Leonardo de Moura
d7abecd07d
test: addDecorations without partial
2022-04-02 19:08:21 -07:00
Leonardo de Moura
c873ad6ef3
test: recursive function on Syntax without partial
2022-04-02 18:43:45 -07:00
Leonardo de Moura
9d55d7bf9e
feat: add helper tactic for applying List.sizeOf_lt_of_mem in termination proofs
2022-04-02 18:38:55 -07:00
Leonardo de Moura
64cfbc1ae3
feat: add helper tactic for applying sizeOf (a.get i) < sizeOf a automatically in termination proofs
2022-04-02 18:29:41 -07:00
Leonardo de Moura
03ec8cb30b
feat: missing sizeOf theorems for Array.get and List.get
2022-04-02 16:04:46 -07:00
Leonardo de Moura
a926cd1698
fix: mkUnfoldProof
...
The hypotheses in an equation theorem may depend on each other
2022-04-01 15:47:24 -07:00
Leonardo de Moura
4a0f68de83
fix: split tactic issue
2022-04-01 15:47:24 -07:00
Leonardo de Moura
0241d7c197
chore: fix tests
2022-04-01 11:34:50 -07:00
Leonardo de Moura
414f5596a6
test: Nat.binrec example
2022-04-01 08:29:44 -07:00
E.W.Ayers
4c2fedae50
doc: fix @Kha's issues with MonadControl
2022-04-01 10:06:58 +02:00
Leonardo de Moura
096e4eb6d0
fix: equation generation for nested recursive definitions
...
The issue was raised on Zulip. The issue is triggered in
declarations containing overlapping patterns and nested recursive
definitions occurring as the discriminant of `match`-expressions.
Recall that Lean 4 generates conditional equations for declarations
containing overlapping patterns.
To address the issue we had to "fold" `WellFounded.fix` applications
back as recursive applications of the functions being defined.
The new test exposes the issue.
2022-03-31 17:04:06 -07:00
Leonardo de Moura
6652d2665d
chore: remove old comment
2022-03-31 15:59:31 -07:00
Leonardo de Moura
734902bd3c
test: add split list example from Zulip without sorrys
2022-03-31 13:03:58 -07:00
Leonardo de Moura
2bd04285f8
fix : #1087
...
This commit is using the easy fix described at issue #1087 .
Hopefully the performance overhead is small.
closes #1087
2022-03-30 18:48:02 -07:00
Leonardo de Moura
63b9060ce9
chore: fix comments
2022-03-30 16:23:06 -07:00
Leonardo de Moura
3dd0c84c4d
chore: enforce naming convetion for tactics
2022-03-30 16:19:05 -07:00
Leonardo de Moura
a509b0c615
test: Sign
2022-03-30 13:33:29 -07:00
Leonardo de Moura
1a8840330f
test: add test for example that does not work in Lean3
...
cc @eric-wieser
2022-03-30 12:59:55 -07:00
Leonardo de Moura
e53e088be8
test: make it clear the proofs hold by reflexivity
2022-03-30 12:40:30 -07:00
Leonardo de Moura
6056a4cbfa
test: stars_and_bars
2022-03-30 12:38:05 -07:00
Leonardo de Moura
86432f1833
feat: improve let-pattern and have-pattern macro expansion
2022-03-29 07:33:22 -07:00
Leonardo de Moura
c7321e0061
chore: remove revert hack from example
2022-03-28 17:18:36 -07:00
Leonardo de Moura
a06cd40e29
feat: improve match expression support at simp
2022-03-28 17:17:01 -07:00
Leonardo de Moura
3c964f3b9f
feat: substitute auxiliary equations introduced by the split tactic
2022-03-28 14:29:28 -07:00
Leonardo de Moura
314bd3ae4c
fix: simpH? at match expression equation theorem generator
...
closes #1080
2022-03-28 12:48:54 -07:00
Leonardo de Moura
2dea5471da
feat: add support for HEq to the subst tactic
2022-03-28 12:23:55 -07:00
Leonardo de Moura
4e008cf8b7
chore: move to tests
2022-03-27 14:57:33 -07:00
Leonardo de Moura
4801b37cfb
fix: exfalso
2022-03-27 14:56:24 -07:00
Leonardo de Moura
a2e467eb32
fix: mkEqnTypes
...
stop as soon as `lhs` and `rhs` are definitionally equal, and avoid
unnecessary case analysis.
This commit fixes the last issue exposed by #1074
fixes #1074
2022-03-25 19:13:21 -07:00
Leonardo de Moura
370e9c421f
fix: bug at deriving Hashable
2022-03-24 18:46:10 -07:00
Leonardo de Moura
fdbe893c40
fix: catch mkAppM exceptions
2022-03-23 17:35:04 -07:00
Leonardo de Moura
6007147d71
fix: allow universes to be postponed further
...
closes #1058
2022-03-22 13:57:58 -07:00
Leonardo de Moura
9944feb095
test: use [reducible]
2022-03-21 07:39:44 -07:00
Leonardo de Moura
3a75cf1920
test: nested inductives
2022-03-21 05:57:02 -07:00
Leonardo de Moura
a2690d5278
feat: improve #eval command
2022-03-20 15:18:47 -07:00
Leonardo de Moura
7b1091770c
test: Repr for HList
2022-03-20 15:05:34 -07:00
Leonardo de Moura
6d926c7989
feat: macro expand match alternatives
...
see #371
This commit does not implement all features discussed in this issue.
It has implemented it as a macro expansion. Thus, the following is
accepted
```lean
inductive StrOrNum where
| S (s : String)
| I (i : Int)
def StrOrNum.asString (x : StrOrNum) :=
match x with
| I a | S a => toString a
```
It may confuse the Lean LSP server. The `a` on `toString` shows the
information for the first alternative after expansion (i.e., `a` is an `Int`).
After expansion, we have
```
def StrOrNum.asString (x : StrOrNum) :=
match x with
| I a => toString a
| S a => toString a
```
2022-03-20 14:20:13 -07:00
Leonardo de Moura
87bb299f08
feat: add Iterator.atEnd
2022-03-20 11:40:46 -07:00
E.W.Ayers
d954706fcf
feat: ApplyNewGoals config for apply
...
Lean.Meta.Tactic.apply now accepts an ApplyConfig argument.
`apply` now changes which metavariables are stored with choice
of the newGoals config.
This allows one to implement `fapply` and `eapply`.
An example of this is given in tests/lean/run/apply_tac.lean.
Closes #1045
2022-03-19 15:51:40 -07:00
Leonardo de Moura
4f318d3304
test: use dot notation in the example
2022-03-19 10:39:58 -07:00
Leonardo de Moura
d1eb180aae
test: add non mutually recursive version
2022-03-19 10:38:39 -07:00
Leonardo de Moura
bdb2e9597a
chore: naming convention
2022-03-19 10:20:42 -07:00
Leonardo de Moura
6c8322d20a
test: use builtin Char.isDigit and Char.toNat
2022-03-19 10:18:34 -07:00
Leonardo de Moura
a8ddb56e0e
chore: cleanup David's example
2022-03-19 10:13:27 -07:00
Leonardo de Moura
c95d5f25a3
feat: convert ites into dites in the WF module
...
Motivation: the condition is often used in termination proofs.
2022-03-19 10:11:50 -07:00
Leonardo de Moura
c7cdbf8ff8
feat: improve auto generated termination_by a bit
2022-03-19 09:28:19 -07:00
Leonardo de Moura
64c5cda612
test: David's lex with string iterators
2022-03-19 09:15:29 -07:00
Leonardo de Moura
9722aeaf32
feat: use String.Iterator.sizeOf_next_lt in the builtin decreasing_tactic
2022-03-19 09:04:40 -07:00
