larsk21
70aff92f8f
fix: short-circuit ignore functions in unused variables linter
2022-07-13 10:35:37 +02:00
larsk21
9fcae6ffe9
fix: replace constant with opaque
2022-07-13 10:35:37 +02: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
a0e459999b
chore: cleanup
2022-07-12 17:36:04 -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
Leonardo de Moura
ca4bd67746
chore: cleanup
2022-07-12 16:42:31 -07:00
Leonardo de Moura
b8ed579289
fix: fixes #1300
2022-07-12 14:08:47 -07:00
Leonardo de Moura
1235832314
feat: add runPendingTacticsAt (e : Expr)
2022-07-12 14:07:55 -07:00
Leonardo de Moura
e03e0bd254
refactor: split syntheticMVars into a map and todo-stack
2022-07-12 13:07:36 -07:00
Leonardo de Moura
64dbbb50f8
chore: cleanup
2022-07-12 09:26:00 -07:00
Leonardo de Moura
309f8d6bf9
fix: implicit arguments must be processed with at least default transparency
...
see #1299
2022-07-11 19:11:46 -07:00
Leonardo de Moura
5bd1f7bba1
fix: special support for higher order output parameters at isDefEqArgs
...
closes #1299
2022-07-11 19:05:24 -07:00
Leonardo de Moura
4d81c609cc
chore: cleanup
2022-07-11 18:52:55 -07:00
Leonardo de Moura
3fd2250799
feat: add higherOrderOutParam to ParamInfo
...
Helper info for #1299
2022-07-11 18:52:01 -07:00
Leonardo de Moura
709f22c8e4
feat: add field dependsOnHigherOrderOutParam to ParamInfo
...
See issue #1299
2022-07-11 17:49:49 -07:00
Leonardo de Moura
f657aed798
feat: store outParam positions
2022-07-11 17:21:31 -07:00
Leonardo de Moura
dfc88ef99f
chore: use a[i]
2022-07-11 16:44:52 -07:00
Gabriel Ebner
a8cab84735
refactor: use computed fields for Expr
2022-07-11 14:19:41 -07:00
Gabriel Ebner
eba400543d
refactor: use computed fields for Name
2022-07-11 14:19:41 -07:00
Gabriel Ebner
3176943750
refactor: use computed fields for Level
2022-07-11 14:19:41 -07:00
Gabriel Ebner
23113501f4
chore: prepare for Name refactoring
2022-07-11 14:19:41 -07:00
Gabriel Ebner
c100f45b77
feat: add simp lemmas and instances for LawfulBEq
2022-07-11 14:19:41 -07:00
Gabriel Ebner
a7e8a82e89
chore: require @[computedField] attribute
2022-07-11 12:26:53 -07:00
Gabriel Ebner
6fe3e36804
feat: support extern computed fields
2022-07-11 12:26:53 -07:00
Gabriel Ebner
243439a75c
feat: support modifiers in computed fields
2022-07-11 12:26:53 -07:00
Gabriel Ebner
3a55228be0
chore: prepare for bootstrapping
2022-07-11 12:26:53 -07:00
Gabriel Ebner
b1eb022027
feat: computed fields
2022-07-11 12:26:53 -07:00
Gabriel Ebner
b48061ed23
feat: expose lower level compile function
2022-07-11 12:26:53 -07:00
Gabriel Ebner
18a299f576
feat: allow implementedBy on constructors and casesOn
2022-07-11 12:26:53 -07:00
Gabriel Ebner
5024c15a7a
feat: add getConstInfoDefn
2022-07-11 12:26:53 -07:00
Gabriel Ebner
3776e3c925
feat: generalize unsafeCast to Sort
2022-07-11 12:26:53 -07:00
Leonardo de Moura
c568f11ddf
feat: use default transparency at isDefEqProofIrrel
...
closes #1302
2022-07-11 12:11:10 -07:00
Leonardo de Moura
2fcd406f99
chore: remove sorry
2022-07-10 20:04:06 -07:00
Leonardo de Moura
ee0735760a
feat: add instance : GetElem (List α) Nat α fun as i => i < as.length
2022-07-10 17:38:59 -07:00
Leonardo de Moura
0c5dfd78d7
chore: style
2022-07-10 15:26:26 -07:00
Leonardo de Moura
475c7e18cd
chore: missing GetElem instances
2022-07-10 14:53:22 -07:00
Leonardo de Moura
4173a863d8
chore: cleanup
2022-07-10 09:43:12 -07:00
Leonardo de Moura
451abdf79d
fix: Level.update* functions
...
see #1291
2022-07-10 09:16:02 -07:00
Leonardo de Moura
ba606debf7
fix: Expr.update* issue
...
See #1291
2022-07-10 08:33:14 -07:00
Leonardo de Moura
f1d84a5096
perf: use dsimp := false in split tactic and while proving equation theorems
...
It is just a waste in these two cases.
It now takes 0.78 secs to process example on issue #1287 .
closes #1287
2022-07-10 08:03:42 -07:00
Leonardo de Moura
4b543d5edd
feat: add option for disabling dsimp during simp
2022-07-10 07:57:41 -07:00
Leonardo de Moura
394d49da58
perf: Expr.hasSorry and similar functions
...
Functions were ignoring sharing while traversing `Expr`.
Addresses performance problem exposed by #1287
2022-07-10 07:39:38 -07:00
Leonardo de Moura
2f1b80721e
chore: avoid a[i]' h notation
2022-07-10 07:20:07 -07:00
Leonardo de Moura
35018dbea2
feat: unexpanders for a[i], a[i]' h, a[i]!, and a[i]?
2022-07-10 06:47:23 -07:00
Leonardo de Moura
23bae264fd
perf: add cache for check (e : Expr) : MetaM Unit
...
Address one of the performance problems exposed by #1287
2022-07-09 20:09:15 -07:00
Leonardo de Moura
881589fc46
chore: remove parser workarounds
2022-07-09 16:42:39 -07:00
