Leonardo de Moura
3f0a9eb424
test: add test for issue #1253
...
closes #1253
2022-06-27 09:56:47 -07:00
Leonardo de Moura
c498285d94
chore: add missing double backtick
2022-06-27 09:56:47 -07:00
Sebastian Ullrich
3eeeca22e2
chore: lean-gdb: recursive values & tag
2022-06-26 18:47:47 +02:00
Sebastian Ullrich
5a0c3b8d80
fix: String.isNat
2022-06-25 18:42:08 +02:00
Wojciech Nawrocki
aacfd11508
feat: boolean inequality lemmas
2022-06-25 11:18:09 +02:00
E.W.Ayers
cc9293af09
doc: isDefEq explain mvar levels
2022-06-24 15:24:52 -07:00
Sebastian Ullrich
8979ed42a4
refactor: file worker: wait on header task before dispatching requests
2022-06-24 19:02:00 +02:00
Sebastian Ullrich
e14b4ab0e4
feat: file worker: make header snapshot asynchronous
2022-06-24 19:02:00 +02:00
Leonardo de Moura
220d2e3816
feat: add filterTR and [csimp] theorem
2022-06-24 06:40:38 -07:00
Leonardo de Moura
1fd2b17a92
fix: bug at addDependencies
...
closes #1247
2022-06-24 06:20:00 -07:00
Gabriel Ebner
ec4200fc75
chore: remove unnecessary ppLine
2022-06-24 10:59:55 +02:00
Gabriel Ebner
233a787e65
chore: add test for sepByIndent.formatter
2022-06-24 10:59:55 +02:00
Gabriel Ebner
d5142ddeb8
chore: add sepByIndent.formatter
2022-06-24 10:59:55 +02:00
Gabriel Ebner
733f220ee3
feat: $[...]* antiquotations for sepByIndent
2022-06-24 10:59:55 +02:00
Leonardo de Moura
09c4af26fc
fix: ConstantInfo.all for consistency
2022-06-23 16:41:54 -07:00
Leonardo de Moura
88fae4e3d6
chore: update stage0
2022-06-23 16:41:05 -07:00
Leonardo de Moura
98c775da34
feat: save mutual block information for definitions/theorems/opaques
2022-06-23 16:39:51 -07:00
Leonardo de Moura
ea3e27bbc4
chore: update stage0
2022-06-23 16:13:49 -07:00
Leonardo de Moura
69a446c8d1
feat: add field all to DefinitionVal and TheoremVal
...
Remark: we need an update stage0, and the field is not being updated
correctly set yet.
2022-06-23 16:13:26 -07:00
Leonardo de Moura
da63e003e7
chore: update stage0
2022-06-23 13:32:13 -07:00
Leonardo de Moura
1e4e683e91
chore: update stage0
2022-06-23 13:30:04 -07:00
Henrik Böving
0fde2db75e
feat: improve the heuristic for notation delab
...
Instead of the previous constraints on the right hand side that only
allowed a permutation of variables as parameters to a function the
new heuristic allows anything to the right of a function as long as
each variable only appears at most once.
2022-06-23 13:27:53 -07:00
Leonardo de Moura
3a89723f8c
chore: update stage0
2022-06-23 10:23:37 -07:00
Leonardo de Moura
96a72d67f2
fix: avoid unnecessary dependencies at mkMatcher
...
fixes #1237
2022-06-23 10:21:32 -07:00
Leonardo de Moura
17fa60e1ec
chore: remove dead code
2022-06-23 09:31:52 -07:00
Sebastian Ullrich
17c2e6d529
feat: publish fatal progress after worker crash
2022-06-23 09:24:27 -07:00
Connor Baker
c213e0e880
doc: fix overwide view when using Alectryon
2022-06-23 18:23:28 +02:00
Leonardo de Moura
939f8d9f16
fix: fixes #1240
2022-06-23 05:53:06 -07:00
Sebastian Ullrich
1f13729756
feat: show term goal at end of term as well
2022-06-23 14:44:19 +02:00
Sebastian Ullrich
13bcbce144
chore: fix Nix test output filter
2022-06-23 14:05:53 +02:00
Sebastian Ullrich
1712d0fee3
chore: update LeanInk
...
Resolves leanprover/LeanInk#20
2022-06-23 11:32:16 +02:00
Leonardo de Moura
108bc4c27f
fix: extCore
2022-06-22 19:40:06 -07:00
Leonardo de Moura
a84b9b2e7b
doc: update release notes
2022-06-22 19:34:29 -07:00
Leonardo de Moura
53acd3e355
feat: allow ext conv tactic to go inside let-declarations
2022-06-22 19:27:04 -07:00
Leonardo de Moura
4d1c6dd557
feat: add zeta conv tactic
2022-06-22 19:15:10 -07:00
Leonardo de Moura
a802544c90
fix: intro tactic at let-expr
2022-06-22 16:10:33 -07:00
Leonardo de Moura
2a940dd4ae
feat: add Expr.collectFVars, LocalDecl.collectFVars, Pattern.collectFVars, and AltLHS.collectFVars
...
They are all in `MetaM`.
These are helper functions for issue #1237 . We need to "cleanup" the
local context before trying to compile the match-expression.
see issue #1237
2022-06-22 15:53:43 -07:00
Leonardo de Moura
9678be4d81
fix: store discharge depth when caching simp results
...
Closes #1234
2022-06-21 15:35:47 -07:00
Leonardo de Moura
65d24f4e39
fix: typo at LinearExpr.toExpr
...
closes #1236
2022-06-21 14:28:26 -07:00
Sebastian Ullrich
71b99423e8
chore: Nix: fix CI
2022-06-21 23:11:57 +02:00
Sebastian Ullrich
02e5865a02
chore: Nix: stop pinning Nix in ciShell
2022-06-21 22:57:39 +02:00
Sebastian Ullrich
ce73728be3
chore: Nix: avoid build closure dependencies on stdenv
2022-06-21 21:11:59 +02:00
Sebastian Ullrich
dd58b5c2df
chore: Nix: cache correct output
2022-06-21 21:10:08 +02:00
Sebastian Ullrich
e20f2e076e
chore: Nix: cache lean-bin-tools
2022-06-21 20:52:39 +02:00
Leonardo de Moura
e442fbbf54
fix: remove kabstractWithPred
...
The function `kabstractWithPred` was never used, and introduced the
bug exposed by issue #1235 .
fixes #1235
2022-06-20 16:35:18 -07:00
Leonardo de Moura
986de33097
fix: fixes #1230
2022-06-20 09:58:27 -07:00
E.W.Ayers
b6f251bcd3
fix: SubExpr.Pos.toString not terminating
...
fixes 1232
2022-06-19 16:04:50 -07:00
Sebastian Ullrich
58d5a11928
Revert "fix: induction: do not register _ as binder in info tree"
...
This reverts commit 143b2b49c8
2022-06-18 17:24:08 +02:00
Sebastian Ullrich
99607c208c
Revert "fix: intro/intros: do not register _ as binder in info tree"
...
This reverts commit 41dfd06e8c
2022-06-18 17:24:08 +02:00
Sebastian Ullrich
a4236c0721
fix: ignore hygiened names in unused variables linter
2022-06-18 17:24:08 +02:00
