Leonardo de Moura
d9d893e425
chore: fix test
2022-07-24 18:07:54 -07:00
Leonardo de Moura
b6e9d58537
feat: add [deprecated] attribute
2022-07-24 18:06:03 -07:00
Leonardo de Moura
a62949c49b
refactor: add type LevelMVarId (and abbreviation LMarId)
...
Motivation: make sure we do not mixup metavariable ids for
expression and universe level.
cc @bollu
2022-07-24 17:21:45 -07:00
Leonardo de Moura
e0882e098b
chore: avoid stackoverflow in debug build
2022-07-24 14:47:51 -07:00
Leonardo de Moura
2c825de6a1
fix: elim_scalar_array_cases
2022-07-24 14:46:46 -07:00
Leonardo de Moura
5e877b115b
feat: improve calc tactic
...
> Heather suggested changing the calc tactic (not the term) such that if
the final RHS does not defeq match the goal RHS, it returns a final
inequality as a subgoal.
Closes #1342
2022-07-24 14:30:15 -07:00
Leonardo de Moura
c46ef56ac7
perf: avoid blowup at deriving Repr
...
The fix is not perfect. I just avoided inlining in some builtin `Repr` instances.
The actual problem is at `ElimDeadBranches.lean`.
Closes #1365
2022-07-24 13:10:04 -07:00
Leonardo de Moura
5253cc6742
fix: compiler support for FloatArray.casesOn and ByteArray.casesOn
...
closes #1311
2022-07-24 12:36:08 -07:00
Leonardo de Moura
7829be9d54
fix: fixes #1333
2022-07-24 12:19:53 -07:00
Leonardo de Moura
2196a3518e
perf: improve lazy_delta_reduction_step heuristic
...
It addresses a performance issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/performance.20of.20equality.20with.20projections.2Fmutual/near/288083209
2022-07-24 11:48:45 -07:00
Leonardo de Moura
6cff1f1813
fix: try to postpone by .. if expectedType? = none
...
Reason: it may become `some ..` later. See issue #1359
Closes #1359
2022-07-24 08:03:25 -07:00
Leonardo de Moura
28fc2f9d37
fix: improve "{varName} cannot be reassigned" error message
...
closes #1341
2022-07-24 07:44:34 -07:00
Leonardo de Moura
ad5ee05a03
chore: consistent use of backticks in error messages at Do.lean
2022-07-24 07:42:04 -07:00
Leonardo de Moura
8de798c4a6
feat: reject [macroInline] declarations in recursive declarations
...
closes #1363
2022-07-24 07:26:35 -07:00
Sebastian Ullrich
5160cb7b0f
refactor: remove some unnecessary antiquotation kind annotations
2022-07-23 17:09:32 +02:00
Mario Carneiro
f6211b1a74
chore: convert doc/mod comments from /- to /--//-! ( #1354 )
2022-07-22 12:05:31 -07:00
Leonardo de Moura
8f4ad15a47
fix: ensure messages associated with last exception are not lost at evalTactic
...
closes #1358
2022-07-22 12:05:29 -04:00
Sebastian Ullrich
1f081ee6cb
feat: doc comment support for unif_hint
2022-07-22 14:30:49 +02:00
Sebastian Ullrich
5d187b8beb
fix: register tokens in parser quotation
2022-07-21 23:49:57 +02:00
Sebastian Ullrich
563d42f6d6
fix: make foApprox mdata-invariant
2022-07-21 14:05:47 -07:00
Andrés Goens
b36b50adb2
feat: syntax for using while condition in proofs
2022-07-21 16:57:35 +00:00
Leonardo de Moura
64b7b857f1
chore: ICERM attribute demo
2022-07-21 07:38:47 -04:00
Leonardo de Moura
b581c2fa17
fix: evalTactic
...
Another bug reported by Patrick.
2022-07-20 19:12:53 -04:00
E.W.Ayers
5bf5abe84f
test: update 533 test to include docstring
2022-07-20 15:30:30 -07:00
Sebastian Ullrich
c43a84ca30
fix: unsafe initialize
2022-07-20 22:37:01 +02:00
Mario Carneiro
a2ef6bd19e
fix: malformed/misaligned markdown code fences
2022-07-20 11:12:42 +02:00
Leonardo de Moura
3846dd60fd
fix: evalTactic
...
This commit fixes bug reported by Patrick Massot.
It happened when using `macro_rules` and `elab_rules` for the same
`SyntaxNodeKind`.
It also fixes missing error messages when there is more than one
elaboration functions and there is `abortTactic` exception.
Remark: this commit also changes the evaluation order. Macros are
now tried before elaboration rules. The motivation is that macros are
already applied before elaboration functions in the term elaborator.
2022-07-19 23:28:14 -04:00
Gabriel Ebner
f2e7cbfbaf
chore: use inaccessible name for RpcEncodingPacket
2022-07-19 22:55:42 +02:00
Gabriel Ebner
4ce56f7c05
fix: use field names if specified
2022-07-19 22:55:42 +02:00
Gabriel Ebner
59f528e678
fix: support empty inductives in json derive
2022-07-19 22:55:42 +02:00
Gabriel Ebner
2c0f8fac99
feat: support unused params in RpcEncoding deriver
2022-07-19 22:55:42 +02:00
Gabriel Ebner
ed5e0f098c
fix: support non-type params in RpcEncoding
2022-07-19 22:55:42 +02:00
Gabriel Ebner
62ede1fdfd
chore: update test
2022-07-19 22:55:42 +02:00
Gabriel Ebner
bffd762822
feat: improve RpcEncoding derive test
2022-07-19 22:55:42 +02:00
Gabriel Ebner
eda3eae18e
perf: implement Expr.update* in Lean
2022-07-19 05:55:13 -07:00
Sebastian Ullrich
987785242f
fix: disable auto implicits in structure field default values
2022-07-18 21:09:56 -07:00
Leonardo de Moura
73fce217f6
test: for issue #1321
2022-07-18 23:50:41 -04:00
Leonardo de Moura
3325987be4
chore: fix tests
2022-07-18 23:18:59 -04:00
Gabriel Ebner
3edf22f3f5
fix: crash in binop%
2022-07-17 09:57:56 -07:00
Gabriel Ebner
ff3c67d1ad
feat: recover from errors in attributes
2022-07-16 06:19:54 -07:00
Gabriel Ebner
69da058c03
fix: tests/lean/625.lean
2022-07-16 06:19:54 -07:00
Leonardo de Moura
fb9b093cf9
chore: update example
2022-07-13 15:15:00 -07:00
Leonardo de Moura
94df25e99b
chore: update example
2022-07-13 15:13:31 -07:00
Leonardo de Moura
cce2d3500e
test: for issue #1301
...
closes #1301
2022-07-13 06:05:12 -07:00
larsk21
15f9c0585a
fix: consider macro expansions in unused variables linter
2022-07-13 10:35:37 +02:00
larsk21
ced8df3e86
fix: references of variables with equal ranges
2022-07-13 10:35:37 +02:00
Leonardo de Moura
b6860968ff
fix: catch exception at elabMutualDef
...
closes #1301
2022-07-12 18:39:30 -07:00
Leonardo de Moura
fdef55339f
fix: use binop% for elaborating ^
...
closes #1298
2022-07-12 18:20:02 -07:00
Leonardo de Moura
5e333191a2
feat: improve binop% and binrel% elaboration functions
...
Add support for operators that may not have homogeneous instances for
all types. For example, we have `HPow Nat Nat Nat` and `HPow Int Nat Int`,
but we don't have `HPow Int Int Int`.
2022-07-12 18:12:20 -07:00
Leonardo de Moura
d1f0db7072
fix: resumePostponed backtracking
...
Note that test for issue #1200 broke.
The bug fixed by this commit was allowing the example to be elaborated
correctly :(
Initially, the type of the discriminant is not available, and
`.none (α:=α)` can only be elaborated when the expected type is of the
form `C ...`. Lean then tries to elaborate the alternatives, learn
that the discriminant should be `Option ?m`, and fails because the
patterns still have metavariables after elaboration. Before the bug
fix, `resumePostpone` was **not** restoring the metavariable context,
and the assingnment would stay there. With this information, Lean
can now elaborate `.none (α:=α)`.
Although the bug had a positive impact in this case, it produced
incorrect behavior in other examples.
The fixed example looks reasonable. Thus, we will not reopen
issue #1200
2022-07-12 16:52:45 -07:00
