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
Sebastian Ullrich
8aea00213c
chore: clean up doc/flake.nix
2022-06-18 13:21:02 +02:00
Wojciech Nawrocki
7624e25de0
fix: don't duplicate tags in formatter
2022-06-18 10:07:53 +02:00
Wojciech Nawrocki
b1ef58d3cc
fix: tag idents so that ofFieldInfo nodes are preserved
2022-06-18 10:07:53 +02:00
E.W.Ayers
ee6ba180ea
fix: remove fix2
2022-06-17 17:47:51 -07:00
E.W.Ayers
18ba16ded9
feat: string representation of Pos
...
This is needed because JSON will otherwise lossily
convert big nats to floats.
2022-06-17 17:47:51 -07:00
E.W.Ayers
933964f2a4
chore: rm SubExpr.mapPos because it is not useful
2022-06-17 17:47:51 -07:00
E.W.Ayers
114bbc78ed
test: numBinders
2022-06-17 17:47:51 -07:00
E.W.Ayers
8b1130c6dd
test: replaceSubexpr pure p e = e
...
This found a bug in lensCoord which I fixed.
2022-06-17 17:47:51 -07:00
E.W.Ayers
b110d800e9
fix: add ExprTraversal to Meta
2022-06-17 17:47:51 -07:00
E.W.Ayers
4a70143aaf
style: minor formatting changes
2022-06-17 17:47:51 -07:00
E.W.Ayers
3c14c97195
test: add unit test for Expr lens
2022-06-17 17:47:51 -07:00
E.W.Ayers
a7c33a963f
doc: docstrings for List.isPrefixOf
2022-06-17 17:47:51 -07:00
E.W.Ayers
0707e4d442
fix: traverseChildrenWithPos bug
2022-06-17 17:47:51 -07:00
E.W.Ayers
0e84f67d99
feat: with pos expr traversal functions
2022-06-17 17:47:51 -07:00
E.W.Ayers
562070fe8b
refactor: more extract methods from transform
2022-06-17 17:47:51 -07:00
E.W.Ayers
c8fc371eb9
fix: test
2022-06-17 17:47:51 -07:00
E.W.Ayers
8311c88fd0
refactor: extract methods from Lean.Meta.transform
...
Lean.Meta.transform is created with a series of recursive
visit functions. However these visit functions are useful
on their own outside of transform for traversing expressions.
This commit moves the visit functions outside the main function.
2022-06-17 17:47:51 -07:00
E.W.Ayers
ece1c1085c
feat: add Expr lensing functions using SubExpr.Pos
2022-06-17 17:47:51 -07:00
E.W.Ayers
2fe933cdf5
refactor: make SubExpr.Pos a definition
...
Instead of an abbreviation. It is easier to understand
Pos operations in terms of 'push' and 'pop' rather than
through arithmetic.
2022-06-17 17:47:51 -07:00
Leonardo de Moura
bbc196eeb7
fix: make sure WF/Fix.lean tolerates MatcherApp.addArg? failures
...
see #1228
2022-06-17 17:37:33 -07:00
Leonardo de Moura
52a0de00e4
feat: report error on ambiguous export and open commands
...
This commit improves the fix for issue #1224
2022-06-17 09:58:36 -07:00
Leonardo de Moura
e985eb2b8a
fix: refine resolveNamespace
...
see issue #1224
2022-06-17 09:51:00 -07:00
Leonardo de Moura
f0e2696ec8
doc: update release notes
2022-06-16 18:22:23 -07:00
Leonardo de Moura
81a685d97c
test: issue #1224
...
closes #1224
2022-06-16 18:01:09 -07:00
Leonardo de Moura
a6462f5bd8
feat: improve open/export
2022-06-16 18:00:33 -07:00
Leonardo de Moura
d5476fb3b3
refactor: move toMessageList, add throwErrorWithNestedErrors
2022-06-16 18:00:09 -07:00
Leonardo de Moura
8ca3e14651
feat: change namespace resolution procedure
...
see #1224
2022-06-16 17:31:49 -07:00
Leonardo de Moura
d56163bd0e
refactor: resolveNamespace now return a List
2022-06-16 17:16:36 -07:00
François G. Dorais
bc206b2992
fix: LawfulBEq class
...
make arguments implicit and protect `LawfulBEq.rfl`
2022-06-16 15:33:32 -07:00
Leonardo de Moura
8d9428261e
chore: remove Fix.lean
...
see #1208
2022-06-16 15:30:47 -07:00
Leonardo de Moura
9e7a6fa085
chore: remove dead structure
2022-06-16 15:23:23 -07:00
Sebastian Ullrich
b1e3607739
fix: match tactic with multiple LHSs
2022-06-16 15:21:46 -07:00
Sebastian Ullrich
0777d01cf9
chore: update Lake
2022-06-16 23:33:57 +02:00
Sebastian Ullrich
72a5c582cf
chore: Nix: ignore build messages in test capture
2022-06-16 23:33:57 +02:00
Sebastian Ullrich
4212cc740b
refactor: move linebreak check into sepBy(1)Indent
...
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
2022-06-16 23:33:57 +02:00
Sebastian Ullrich
6f096e0f0d
chore: fix tests
2022-06-16 23:33:57 +02:00
Sebastian Ullrich
6982536108
fix: one more struct instance syntax manipulation
2022-06-16 23:33:57 +02:00
Sebastian Ullrich
0f6e6c8a51
chore: update stage0
2022-06-16 23:33:57 +02:00
Sebastian Ullrich
b585b2251e
fix: adapt to stricter grammar
2022-06-16 23:33:57 +02:00
