Wojciech Nawrocki
11e10459bb
refactor: move function to PrettyPrinter
2022-05-12 08:38:09 -07:00
Wojciech Nawrocki
81b1f1df6e
refactor: unify format functions
2022-05-12 08:38:09 -07:00
Wojciech Nawrocki
aa2ad384e7
chore: remove old InfoTree ctor
2022-05-12 08:38:09 -07:00
Wojciech Nawrocki
b33eb12328
chore: simplify evaluation and use macro scope instead of namespace
2022-05-12 08:38:09 -07:00
Wojciech Nawrocki
aa5fe5864a
doc: document some Deriving utils
2022-05-12 08:38:09 -07:00
Wojciech Nawrocki
4b3c2b1790
doc: document some meta utilities
2022-05-12 08:38:09 -07:00
Leonardo de Moura
a8032e4173
fix: another mut misbehaving example
...
```
def mutVariableDo2 (list : List Nat) : Nat := Id.run <| do
let mut sum := 0
for _ in list do
sum := sum.add 1 -- first `sum` was not connected, i.e., it was not highlighted when hovering over the second `sum`
pure sum
```
2022-05-12 08:26:07 -07:00
Leonardo de Moura
362961912b
chore: remove unnecessary variable
2022-05-12 06:44:13 -07:00
Leonardo de Moura
f44a701637
chore: style
2022-05-11 15:32:18 -07:00
Sebastian Ullrich
d03f0b3851
fix: set of chained lexical references
2022-05-11 17:32:06 +02:00
Leonardo de Moura
94d2a3ef86
feat: improve error message when failing to infer resulting universe level for inductive datatypes and structures
2022-05-10 18:30:53 -07:00
Leonardo de Moura
c935a3ff6a
feat: improve error location for universe level errors at inductive command
2022-05-10 12:50:01 -07:00
Sebastian Ullrich
392640d292
feat: allow keyword-like projection identifiers
2022-05-10 12:25:30 -07:00
Leonardo de Moura
f58afaaa43
fix: make sure let _ := val and let _ : type := val are treated at letIdDecl
...
closes #1114
2022-05-10 06:52:27 -07:00
Sebastian Ullrich
1b51bab4a1
feat: turn on info trees by default
2022-05-10 06:24:31 -07:00
Leonardo de Moura
7ce0471f28
feat: improve binrel% elaborator
...
It now relies on `binop%` too, and addresses issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Regression.20in.20coercion.20inference/near/281737387
2022-05-09 18:39:52 -07:00
Leonardo de Moura
1768067aa0
doc: document elaboration issue
...
described at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Regression.20in.20coercion.20inference/near/281737387
TODO: improve `binrel%` elaboration function.
2022-05-09 17:39:24 -07:00
Sebastian Ullrich
ff6537be1b
fix: use consistent goal prefix everywhere
2022-05-09 17:49:00 +02:00
Leonardo de Moura
fc03b2fc31
feat: unfold ident,+
2022-05-09 07:09:53 -07:00
Leonardo de Moura
995d4f0979
chore: prepare for unfold ident,+
2022-05-09 07:09:22 -07:00
Leonardo de Moura
e729b32b2b
feat: unfold should fail if it didn't unfold anything
2022-05-09 06:41:17 -07:00
Leonardo de Moura
4875224bd4
feat: unfold tactic tries to reduce match after unfolding
2022-05-09 06:35:40 -07:00
Leonardo de Moura
3cd46888bf
fix: check types using default reducibility at synthInstance?
...
closes #1131
2022-05-08 06:49:14 -07:00
Sebastian Ullrich
91991649bc
fix: connect occurrences of mutable variable inside and outside for in info tree
2022-05-07 15:50:26 -07:00
Sebastian Ullrich
22f8ea147c
fix: propagate position information of variables in do blocks
2022-05-07 15:50:26 -07:00
Sebastian Ullrich
daa9e03e78
fix: combineFvars
2022-05-07 15:50:26 -07:00
Sebastian Ullrich
2f461d201e
fix: info tree of let_delayed
2022-05-07 15:50:26 -07:00
Leonardo de Moura
9043f91d8c
fix: if Tactic.Context.recover == false, we must disable "error to sorry" when elaborating terms in tactics
...
closes #1142
2022-05-07 15:37:12 -07:00
Leonardo de Moura
ab31f9ad5d
fix: fixes #1143
2022-05-07 15:27:34 -07:00
Leonardo de Moura
2c8c20d424
feat: add [eliminator] attribute specifying default recursors/eliminators for the cases and induction tactics
2022-05-07 15:09:42 -07:00
Leonardo de Moura
b5bcf252ce
chore: cleanup
2022-05-07 14:48:22 -07:00
Leonardo de Moura
af5e13e534
feat: improve binop% elaboration function
2022-05-07 10:32:55 -07:00
Leonardo de Moura
38baeaf373
feat: backtrack when applying default instances if subproblems cannot be solved
2022-05-07 09:56:38 -07:00
Leonardo de Moura
8c23bef399
feat: add support for casesOn applications to structural and well-founded recursion modules
2022-05-06 17:12:10 -07:00
Leonardo de Moura
090503cfd5
chore: cleanup
2022-05-06 17:12:10 -07:00
KaseQuark
5ebd6c28db
feat: change "⊢" in conv goals to "|"
2022-05-06 09:35:04 +02:00
Leonardo de Moura
c65537aea5
feat: Option is a Monad again
...
TODO: remove `OptionM` after update stage0
see: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Do.20we.20still.20need.20OptionM.3F/near/279761084
2022-05-04 15:27:42 -07:00
Leonardo de Moura
04d3c6feeb
fix: auto implicit behavior on constructors
2022-05-04 15:04:49 -07:00
Leonardo de Moura
a1af8074c9
feat: improve discriminant refinement procedure
2022-05-04 14:46:43 -07:00
Leonardo de Moura
94b5a9b460
feat: improve split tactic
2022-05-03 17:46:50 -07:00
Joscha
5749fb1474
fix: search for local refs only in current file
...
Fixed by adding the identifier's module as an argument to referringTo.
If the ident is RefIdent.const, this is ignored, but if it is
RefIdent.fvar, referringTo limits its search to the ident's module.
2022-05-03 16:53:03 +02:00
Sebastian Ullrich
e76a2a6d9e
chore: normalize spelling
2022-05-03 10:26:11 +02:00
Leonardo de Moura
94abfdba6c
feat: improve implementedBy errors, and relax type matching test
2022-05-02 08:48:15 -07:00
Leonardo de Moura
fe00dd8f29
fix: missing sanitizeNames at msgToInteractiveAux
2022-05-02 07:35:12 -07:00
Sebastian Ullrich
2f3396e58a
fix: non-termination in deduplication of lexical references
2022-05-02 09:51:14 +02:00
Sebastian Ullrich
09e4c00c68
fix: lexical references through x := e and similar macros
2022-05-01 17:46:05 +02:00
Leonardo de Moura
109363bc7e
fix: closes #1132
2022-05-01 08:18:30 -07:00
Leonardo de Moura
4eb2cfec46
feat: make sure case' ... => tac does not use done after tac
2022-05-01 07:30:11 -07:00
Leonardo de Moura
03524305db
fix: findTag?
...
If there is an exact match, return it.
2022-05-01 07:30:11 -07:00
Sebastian Ullrich
a0678b5f6f
refactor: rename confusing Reference.isDeclaration field
2022-05-01 16:21:15 +02:00
