Leonardo de Moura
bd89bdde8a
fix: core library
...
see #1018
2022-02-15 12:12:56 -08:00
Leonardo de Moura
df584567f5
feat: (generalizing := true) is the default behavior for match-expressions
...
closes #1018
2022-02-15 11:12:04 -08:00
Sebastian Ullrich
e9ee9204c4
chore: update Lake
2022-02-15 19:19:19 +01:00
Sebastian Ullrich
54522006f4
refactor: List.get: take Fin to align with Array.get
...
/cc @leodemoura
2022-02-15 18:41:22 +01:00
Leonardo de Moura
d1e5e4166a
feat: use sorry instead of trying to synthesize Inhabited at error recovery
2022-02-15 09:15:18 -08:00
Leonardo de Moura
f75fdcb19b
feat: when Lean cannot prove termination, then report error and add definition as partial, and if it fails add as axiom
2022-02-15 07:44:27 -08:00
Sebastian Ullrich
4b03666ecc
chore: include orphan file
2022-02-15 09:44:19 +01:00
Leonardo de Moura
f33cb27d1c
doc: update RELEASES.md
2022-02-14 15:58:58 -08:00
Leonardo de Moura
66e0b72c6f
test: notation for providing names to equality proofs in match expressions is not whitespace sensitivity anymore
2022-02-14 15:51:23 -08:00
Leonardo de Moura
409530306c
chore: update stage0
2022-02-14 15:48:11 -08:00
Leonardo de Moura
764a1d9f51
chore: fix tests
2022-02-14 15:47:12 -08:00
Leonardo de Moura
c67ee9fdf4
feat: add pp annotation for match parser
2022-02-14 15:46:52 -08:00
Leonardo de Moura
ffca6975f2
chore: remove bootstrapping workarounds
2022-02-14 15:39:21 -08:00
Leonardo de Moura
42c80c7483
feat: remove whitespace sensitivity at match discriminants
2022-02-14 15:37:40 -08:00
Leonardo de Moura
2a2ad75faa
chore: update stage0
2022-02-14 15:37:01 -08:00
Leonardo de Moura
93b5b74b36
feat: modify notation for providing motive in "match" expressions
2022-02-14 15:36:14 -08:00
Leonardo de Moura
0030208d99
chore: prepare to change builtin syntax
2022-02-14 14:17:24 -08:00
Leonardo de Moura
a0fb412989
chore: update stage0
...
Make sure previous fix is also applied to enumeration types in the
core library.
2022-02-14 12:06:42 -08:00
Leonardo de Moura
07043e73b0
chore: fix tests
2022-02-14 12:06:03 -08:00
Leonardo de Moura
aa63fda835
fix: mark auxiliary noConfusion declarations for enumeration types as [reducible]
...
closes #1016
2022-02-14 12:03:49 -08:00
Leonardo de Moura
ee9fcd30e8
fix: mark Nat.decEq as [reducible]
...
It is used by the `noConfusionType` construction for enumeration types,
and we want it to reduce even when the reducibility setting is
`TransparencyMode.reducible` as for other inductive types.
see issue #1016
2022-02-14 12:00:29 -08:00
Leonardo de Moura
93d5351fba
feat: display reducibility status at #print
2022-02-14 11:52:41 -08:00
Leonardo de Moura
420d0f2a3f
fix: make sure noConfusionTypeEnum and noConfusionEnum fully reduce even reducibility setting is set to TransparencyMode.reducible
...
The previous definition would not fully reduce since `ite` and `dite`
are not tagged as `[reducible]`.
see issue #1016
2022-02-14 11:39:18 -08:00
Sebastian Ullrich
bdbffdaaf7
chore: update Lake
2022-02-14 16:52:54 +01:00
ammkrn
3de18ceb55
doc: document match h:e with syntax
2022-02-14 15:53:37 +01:00
Sebastian Ullrich
340c331da9
chore: CI: ignore diff exit code
2022-02-13 00:04:08 +01:00
Leonardo de Moura
8be916b0cf
doc: update RELEASES.md
2022-02-12 12:08:01 -08:00
Leonardo de Moura
82bce7ebec
fix: declare local instaces occurring in patterns
2022-02-12 12:01:08 -08:00
Leonardo de Moura
32dd3c6b29
feat: use at least default transparency at toCtorWhenK
...
Improves the effectiveness of `simp` when reducing `match`-expr.
2022-02-12 07:56:45 -08:00
Leonardo de Moura
999e80745e
test: add test for already fixed issue reported on Zulip
2022-02-12 07:53:31 -08:00
Leonardo de Moura
0649e5fa8a
feat: Basic model-based solver for linear arithmetic
2022-02-11 18:38:33 -08:00
Leonardo de Moura
37afafad6e
feat: missing Rat functions
2022-02-11 18:24:18 -08:00
Leonardo de Moura
e8c23cdf7e
feat: add cache at Lean/Elab/PreDefinition/WF/PackDomain.lean
2022-02-11 09:52:14 -08:00
Leonardo de Moura
9cfa728eac
chore: remove workaround for issue #1013
2022-02-11 09:32:29 -08:00
Leonardo de Moura
7b3a674555
chore: update stage0
2022-02-11 09:31:02 -08:00
Leonardo de Moura
ab41dd0d83
test: add test for issue #1013
2022-02-11 09:28:46 -08:00
Leonardo de Moura
123e0f42e9
feat: support partial and over applications at WF/PackDomain.lean
...
closes #1013
2022-02-11 09:28:17 -08:00
Sebastian Ullrich
2390691116
chore: remove obsolete workaround
2022-02-11 18:19:59 +01:00
Sebastian Ullrich
80e2e1daa8
test: mutual block not needed
2022-02-11 16:22:13 +01:00
Sebastian Ullrich
c460a2e404
chore: CI: fail when uploading 0 files
2022-02-11 10:11:45 +01:00
Sebastian Ullrich
589f05d2c8
chore: CI: do not delete nightly artifacts before uploading them
2022-02-11 10:02:54 +01:00
Leonardo de Moura
77bbaf82df
feat: decidable equality for arrays
2022-02-10 17:31:03 -08:00
Leonardo de Moura
a2b7ff9e0d
chore: fix doc
2022-02-10 17:12:18 -08:00
Leonardo de Moura
712d6726e4
feat: rename tactic byCases => by_cases
2022-02-10 17:11:07 -08:00
Leonardo de Moura
1491253479
feat: helper simp theorems
2022-02-10 17:06:16 -08:00
Leonardo de Moura
1d5da63482
chore: simplify Array.isEqvAux
2022-02-10 16:51:47 -08:00
Leonardo de Moura
6b6c44c559
feat: add helper lemma
2022-02-10 16:51:32 -08:00
Sebastian Ullrich
894dc0e1b8
fix: pretty-printing match dependent on let
2022-02-10 10:19:04 +01:00
Leonardo de Moura
54473ad523
test: add missing test for issue #998
2022-02-09 18:02:01 -08:00
Leonardo de Moura
9fe0d28107
fix: do not split on if-then-else terms when generating equation theorems
...
Reason: avoid unnecessary case-analysis explosion
It is also unnecessary since we only refine the `below` and `F`
arguments over `match`-expressions.
This fixes the last case at issue #998
```
attribute [simp] BinaryHeap.heapifyDown
```
closes #998
2022-02-09 17:43:35 -08:00
