Leonardo de Moura
0a5df7cd6d
chore: style
2022-07-05 20:45:53 -07:00
tydeu
6e4bca57c8
chore: update Lake
2022-07-05 17:27:41 -07:00
Leonardo de Moura
91d48c9150
chore: update stage0
2022-07-05 14:29:45 -07:00
Leonardo de Moura
627594b88a
fix: "dot"-notation should apply default instances before failing
...
See new test for motivating example.
2022-07-05 14:27:55 -07:00
Leonardo de Moura
13a49da496
chore: update stage0
2022-07-05 13:25:50 -07:00
Leonardo de Moura
2b2d4245dc
fix: extensible tactics bug
...
See comment at `expandMacros`
2022-07-05 13:20:22 -07:00
Siddharth Bhat
e6629b760d
fix: Clearer error message for cast(▸) notation
...
The old error message said:
```
throwError "invalid `▸` notation,
expected type{indentExpr expectedType}\ndoes contain
equation left-hand-side nor right-hand-side{indentExpr heqType}"
```
The phrase `does contain ... nor ..` seems gramatically incorrect.
What was (probably) intended was `does **not** contain ... nor ...`.
We take the opportunity to clean up the error message and
be clearer that the equality does not contain the expected result type.
2022-07-05 09:01:09 -07:00
Sebastian Ullrich
6303fb77d2
fix: expansion info for macro commands
...
TODO: investigate that pp error
2022-07-05 13:18:59 +02:00
tydeu
bff560759e
feat: add missing literal TSyntax helpers
2022-07-05 13:18:58 +02:00
Leonardo de Moura
2061c9bbea
chore: reduce test size
...
TODO: investigate why there is a stack overflow in the CI.
I didn't manage to reproduce it on my machine.
2022-07-04 13:58:06 -07:00
Leonardo de Moura
ffc90f6a35
fix: bug at ll_infer_type
2022-07-04 13:55:55 -07:00
Leonardo de Moura
7668750cb5
chore: update stage0
2022-07-04 07:25:35 -07:00
Leonardo de Moura
1999db1d7c
test: add test for performance issue
...
This issue has bee reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/deterministic.20timeout.20with.20structures/near/288180087
2022-07-04 07:20:12 -07:00
Leonardo de Moura
c434e4e096
chore: remove old tests
2022-07-04 07:18:07 -07:00
Leonardo de Moura
2446c64a99
chore: cleanup
2022-07-04 07:15:04 -07:00
Leonardo de Moura
64edb50687
chore: fix tests
2022-07-04 06:35:21 -07:00
Leonardo de Moura
f77ebae87f
fix: withResetUsedAssignment
2022-07-04 06:33:42 -07:00
Leonardo de Moura
05a28af429
fix: skipDefEqCache
2022-07-04 06:33:32 -07:00
Leonardo de Moura
88fc0b2503
fix: isAssigned-like functions should set usedAssignment
2022-07-04 06:20:37 -07:00
Leonardo de Moura
6b2d2ffac6
fix: preserve usedAssignment flag when replacing MetavarContext
2022-07-04 05:49:54 -07:00
Leonardo de Moura
64d46272c2
fix: do not cache when smart unfolding is disabled
2022-07-04 05:48:35 -07:00
Leonardo de Moura
a1413b8fa1
feat: cache failures at isDefEq
...
We can compile Lean with these changes, but 3 tests are still broken.
This cache is used to address a performance issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/deterministic.20timeout.20with.20structures/near/288180087
2022-07-03 21:52:01 -07:00
Leonardo de Moura
76245b39d1
chore: remove dead field
...
We have remove the old frontend a long time ago.
2022-07-03 15:38:48 -07:00
Leonardo de Moura
aae657571f
doc: docstrings for src/Lean/Meta/Basic.lean
2022-07-03 15:32:15 -07:00
Leonardo de Moura
b78925d9bb
chore: update stage0
2022-07-03 15:01:58 -07:00
Leonardo de Moura
757171db1f
feat: add String.get! and s[i]! notation for String
2022-07-03 14:59:44 -07:00
Gabriel Ebner
07a3cd6980
chore: fix tests
2022-07-03 22:46:59 +02:00
Gabriel Ebner
141b110ff1
feat: add more typed syntax coercions
2022-07-03 22:46:59 +02:00
Gabriel Ebner
922ef23112
fix: do not ignore syntax coercions
...
Syntax coercions do not need to be the identity. See for example
``Coe (TSyntax `ident) (TSyntax `declId)``.
2022-07-03 22:46:59 +02:00
Gabriel Ebner
ddf77a8c6d
chore: style
2022-07-03 22:46:59 +02:00
Gabriel Ebner
bec0bbc351
fix: replace dangerous instance by CoeTail
...
In order to guarantee termination of type class synthesis when resolving
coercions, a good rule of thumb is that the instances should not
introduce metavariables (during TC synthesis). For common coercion type
classes this means:
- `Coe T S`, `CoeTail T S`: the variables of `T` must be a subset of those of `S`
- `CoeHead T S`: the variables of `S` must be a subset of those of `T`
If these rules are not followed, we can easily get nontermination. In
this case: `CoeTC Foo Syntax` is reduced to `CoeTC Foo (TSyntax ?m_1)`
using the (dangerous) `Coe (TSyntax k) Syntax` instance, to which we can
then apply the otherwise fine `Coe (TSyntax [k]) (TSyntax (k'::ks))`
coercion infinitely often.
2022-07-03 22:46:59 +02:00
Gabriel Ebner
3d5c5553d9
fix: add missing coercion instance for CoeHead+CoeTail
2022-07-03 22:46:59 +02:00
Leonardo de Moura
03ce7cb17c
fix: dependent pattern matching bug
...
closes #1279
Originally reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/case.20in.20dependent.20match.20not.20triggering.20.28.3F.29/near/288328239
2022-07-03 13:25:12 -07:00
Leonardo de Moura
68024b11a4
fix: simp_all bug when goal has duplicate hypotheses
2022-07-03 12:44:53 -07:00
Sebastian Ullrich
2f67295c7d
feat: strengthen pp* signatures
2022-07-03 19:14:49 +02:00
Sebastian Ullrich
146aefd085
feat: ppTactic
2022-07-03 19:00:13 +02:00
Sebastian Ullrich
5e46c0865e
doc: update LeanInk
2022-07-03 17:56:51 +02:00
Leonardo de Moura
8f83999202
chore: update release notes
2022-07-03 06:26:47 -07:00
Leonardo de Moura
5e3a3a6c21
chore: remove notation a[i,h] for a[⟨i, h⟩]
2022-07-03 06:24:26 -07:00
kzvi
7326c817d2
fix: fix typos in deBruijn.lean and phoas.lean examples
2022-07-02 16:12:05 -07:00
Leonardo de Moura
0bdab9b4f7
doc: update release notes
2022-07-02 16:06:57 -07:00
Leonardo de Moura
a1d09f1ced
chore: update stage0
2022-07-02 15:57:22 -07:00
Leonardo de Moura
a0fdc2d050
chore: fix tests
2022-07-02 15:57:05 -07:00
Leonardo de Moura
54c60d4c2d
feat: a[i] and a[i]! notation for Subarrays
2022-07-02 15:54:34 -07:00
Leonardo de Moura
a2456c3a0f
feat: add notation a[i, h] for a[⟨i, h⟩]
2022-07-02 15:50:49 -07:00
Leonardo de Moura
eb115abcbe
chore: update stage0
2022-07-02 15:37:13 -07:00
Leonardo de Moura
e81a847ba3
fix: doc/array.md
2022-07-02 15:36:01 -07:00
Leonardo de Moura
4568fe755c
chore: fix tests
2022-07-02 15:25:06 -07:00
Leonardo de Moura
b3ea1fc925
feat: a[i] notation for arrays now uses i : Fin a.size
2022-07-02 15:19:38 -07:00
Leonardo de Moura
e4b472a9a2
chore: fix tests
2022-07-02 15:17:01 -07:00
