Leonardo de Moura
1e59eb2290
chore: update whereStructInst
2022-06-07 18:41:43 -07:00
Leonardo de Moura
041827bed5
chore: unused variables
2022-06-07 17:54:10 -07:00
Leonardo de Moura
c2ddebc193
chore: unused variables
2022-06-07 16:47:04 -07:00
Sebastian Ullrich
f9e2a65f75
chore: further cleanup
...
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
2022-06-07 16:37:45 -07:00
Sebastian Ullrich
8eefbf5227
chore: further clean up refactored code
2022-06-07 16:37:45 -07:00
Sebastian Ullrich
897a5de6ac
chore: revert some questionable signature changes
2022-06-07 16:37:45 -07:00
Sebastian Ullrich
fb2a2b3de2
fix: fixup previous commit
2022-06-07 16:37:45 -07:00
Sebastian Ullrich
ae7b895f7a
refactor: unname some unused variables
2022-06-07 16:37:45 -07:00
Sebastian Ullrich
8ffa07ab25
fix: goal state on conv =>
2022-06-07 17:43:16 +02:00
Sebastian Ullrich
a07e9df66e
fix: use goal prefix in plain goal response
2022-06-07 17:42:09 +02:00
Leonardo de Moura
09ddf76029
feat: simp_all now uses dependent hypotheses for simplification
...
However, it does not simplify them.
closes #1194
2022-06-06 18:31:34 -07:00
Leonardo de Moura
875e71a0d7
chore: unused variables at Simp.lean
2022-06-06 18:24:10 -07:00
Leonardo de Moura
71226243fd
fix: fixes #1192
2022-06-06 18:20:45 -07:00
Leonardo de Moura
0f111da64c
chore: unused variables at Inductive.lean
2022-06-06 18:15:25 -07:00
Leonardo de Moura
5055855637
feat: improve default simp discharge method
...
closes #1193
2022-06-06 17:29:12 -07:00
Leonardo de Moura
3d04899e42
refactor: add unifyEq?
2022-06-06 15:53:40 -07:00
Leonardo de Moura
c9c9b8d835
chore: avoid code duplication
2022-06-06 15:53:40 -07:00
Leonardo de Moura
7dab01be1b
chore: unused eqns
2022-06-06 15:53:40 -07:00
Leonardo de Moura
2832442e7a
fix: unfold declarations tagged with [matchPattern] at reduceMatcher? even if transparency setting is not the default one
...
see #1193
It fixes one of the issues exposed at the issue above.
2022-06-06 15:53:40 -07:00
Leonardo de Moura
e24483d6d3
doc: expand isGenDiseq comment
2022-06-06 15:53:40 -07:00
larsk21
60c8a72262
fix: unused variables linter: consider induction variables as pattern variables
2022-06-06 15:53:10 -07:00
larsk21
a9293410a2
fix: unused variables linter: ignore structure, class and inductive signatures
2022-06-06 15:53:10 -07:00
Wojciech Nawrocki
5b13a4909b
doc: fix transform docstring
2022-06-06 23:06:47 +02:00
Sebastian Ullrich
143b2b49c8
fix: induction: do not register _ as binder in info tree
2022-06-06 23:05:12 +02:00
E.W.Ayers
d55daf80d4
doc: fix misleading SubExpr docstring
2022-06-06 09:37:51 -07:00
Leonardo de Moura
d00d8a2104
fix: typo at copyDefaultValue?
...
see #1190
2022-06-06 07:57:23 -07:00
Leonardo de Moura
22281f25c8
fix: typo at sameHeadSymbol
...
see #1190
2022-06-06 07:46:57 -07:00
Sebastian Ullrich
3c41962275
refactor: Expr.forEach' use in unused variables linter
2022-06-05 14:16:40 +02:00
Sebastian Ullrich
85e0e0ad20
doc: fix Expr.forEach' docstring
2022-06-05 14:16:29 +02:00
Sebastian Ullrich
ec045bfbb8
feat: $_ antiquotation pattern
2022-06-04 13:57:04 +02:00
Sebastian Ullrich
05c5dd4441
fix: unused variables linter: search fvar aliases in tactics
2022-06-03 22:37:38 +02:00
Sebastian Ullrich
f3a7654a63
fix: unused variables linter: find nested uses in tactics
2022-06-03 22:37:38 +02:00
E.W.Ayers
1785ab142e
refactor: move Lean.PrettyPrinter.Delaborator.SubExpr to Lean.SubExpr
...
This is because SubExpr has uses outside the Delaborator.
Closes #1183
2022-06-03 12:38:14 -07:00
Leonardo de Moura
9d6b67eae2
fix: remove check from Simp.synthesizeArgs
...
Some `simp` dischargers can handle metavariables (e.g,
`assumption`). See new test.
closes #1184
2022-06-03 07:40:30 -07:00
Sebastian Ullrich
0b264889ae
fix: goal state on ; after ·
2022-06-03 13:41:04 +02:00
larsk21
caa8804a1d
feat: add nolint options for function arguments and pattern variables
2022-06-03 13:03:52 +02:00
larsk21
93480a3e05
fix: consider tactic mvar assignments for used variables
2022-06-03 13:03:52 +02:00
larsk21
bf907d7b8c
fix: ignore exposed function arguments in unused variables linter
2022-06-03 13:03:52 +02:00
larsk21
57c8c76cd0
fix: use findModuleRefs in unused variables linter
2022-06-03 13:03:52 +02:00
larsk21
b556e73657
refactor: extend Lsp.ModuleRefs in Server.References
2022-06-03 13:03:52 +02:00
larsk21
cf4e106304
fix: unused variables linter review comments
...
- ignore unused variables in dep arrows
- avoid negated options
- make syntax stack generation more performant
- make ignore functions more extensible
- change message severity to `warning`
2022-06-03 13:03:52 +02:00
larsk21
b708eaec2c
fix: forward lean options to workers
2022-06-03 13:03:52 +02:00
larsk21
37d5f8e74a
feat: add unused variables linter
2022-06-03 13:03:52 +02:00
larsk21
8824a479a5
fix: add additional information to Lean.Server.Reference
2022-06-03 13:03:52 +02:00
larsk21
1a1f8f52a5
fix: run linters after elaboration
2022-06-03 13:03:52 +02:00
Leonardo de Moura
8649483b41
feat: produces an error if the declaration body contains a universe parameter that does not occur in the declaration type nor is explicitly provided
...
closes #898
2022-06-02 19:43:09 -07:00
Leonardo de Moura
484e510221
feat: do not use pp.inaccessibleNames = true at getInteractiveTermGoal
...
See discussion at https://github.com/leanprover/vscode-lean4/issues/76
We also use `pp.inaccessibleNames = false` in error messages. In this
setting, an inaccessible name is displayed in the context only if the
target type depends on it.
2022-06-02 16:22:43 -07:00
Leonardo de Moura
878ef3a281
feat: improve acyclic tactic
...
closes #1182
2022-06-02 15:25:14 -07:00
Sebastian Ullrich
1fff412b1f
fix: regressions from previous commit
2022-06-02 19:04:47 +02:00
Sebastian Ullrich
ddfbf6bf9b
fix: show namespace when hovering over declaration name
2022-06-02 18:17:21 +02:00
