Leonardo de Moura
|
95ea0b92ea
|
chore: fix test
|
2022-04-29 12:40:32 -07:00 |
|
Leonardo de Moura
|
d4d538cad8
|
fix: counterexample generation for new match encoding
|
2022-04-29 12:36:53 -07:00 |
|
Leonardo de Moura
|
ec932e389b
|
chore: fix test
|
2022-04-29 12:30:45 -07:00 |
|
Leonardo de Moura
|
d3bc963e92
|
chore: update stage0
|
2022-04-29 12:20:46 -07:00 |
|
Leonardo de Moura
|
6e1c51dd1a
|
feat: splitter proof for new match encoding
|
2022-04-29 12:19:24 -07:00 |
|
Leonardo de Moura
|
89441aac2a
|
feat: match equation theorem generation for new h : discr notation encoding
TODO: splitter theorem generation still needs to be fixed.
|
2022-04-29 11:48:25 -07:00 |
|
Leonardo de Moura
|
24417ed466
|
feat: size, get, get!, getD, and getOp for Subarray
|
2022-04-29 09:55:45 -07:00 |
|
Leonardo de Moura
|
eac83586c6
|
chore: remove leftover
|
2022-04-29 09:10:27 -07:00 |
|
Leonardo de Moura
|
c959c80310
|
chore: reset local context at correct place
|
2022-04-29 09:08:44 -07:00 |
|
Leonardo de Moura
|
10d43492ba
|
chore: fix test
|
2022-04-29 07:17:46 -07:00 |
|
Leonardo de Moura
|
8d9626dab7
|
feat: delaborate match h : d with ...
|
2022-04-29 07:17:46 -07:00 |
|
Leonardo de Moura
|
0f7754847d
|
chore: style
|
2022-04-29 07:17:46 -07:00 |
|
Leonardo de Moura
|
d793d2f0fd
|
feat: adapt elabMatchAltView to handle the new encoding for h : discr = pattern
|
2022-04-29 07:17:46 -07:00 |
|
Leonardo de Moura
|
7a369848a0
|
feat: new mkMatcher
TODO: adjust match elaborator
|
2022-04-29 07:17:46 -07:00 |
|
Leonardo de Moura
|
f4b4b14797
|
refactor: prepare to handle match h: notation at Meta\Match\Match.lean
|
2022-04-29 07:17:46 -07:00 |
|
Sebastian Ullrich
|
9b4feb3d13
|
perf: work around missed TCO
|
2022-04-29 16:16:09 +02:00 |
|
Sebastian Ullrich
|
b450fb8243
|
chore: CI: use stable Nix
|
2022-04-29 16:16:09 +02:00 |
|
Sebastian Ullrich
|
ff4a770c2d
|
feat: annotate match tactic alternatives with expected state
|
2022-04-29 16:16:09 +02:00 |
|
Sebastian Ullrich
|
39a0de40dd
|
feat: annotate <;> with expected state
|
2022-04-29 16:16:09 +02:00 |
|
Sebastian Ullrich
|
0a88f68d39
|
chore: finish with_annotate_state implementation
|
2022-04-29 16:16:09 +02:00 |
|
Sebastian Ullrich
|
d886a1da72
|
chore: update stage0
|
2022-04-29 16:16:09 +02:00 |
|
Sebastian Ullrich
|
db2a912112
|
feat: with_annotate_state helper tactic
|
2022-04-29 16:16:09 +02:00 |
|
Sebastian Ullrich
|
a167828b79
|
fix: refine previous commit's heuristic
Show indented state if there is no outer state that is leading & not indented
relative to the cursor position
|
2022-04-29 16:16:09 +02:00 |
|
Sebastian Ullrich
|
87b216a8e1
|
fix: do not show states from tactics indented further than the cursor
|
2022-04-29 16:16:09 +02:00 |
|
Sebastian Ullrich
|
cc5e7ee731
|
test: part of #1119
|
2022-04-29 16:16:09 +02:00 |
|
Sebastian Ullrich
|
b714a32d27
|
fix: revert "fix: show single final state after tactic combinator"
This reverts commit eb7bf2b272.
|
2022-04-29 16:16:09 +02:00 |
|
Sebastian Ullrich
|
78bf398830
|
fix: avoid signal-unsafe fprintf in stack overflow handler
|
2022-04-29 15:55:11 +02:00 |
|
Vincent de Haan
|
20e16f1c75
|
doc: add amssymb package to latex example to make it work in all cases
|
2022-04-28 11:21:12 +02:00 |
|
Leonardo de Moura
|
575b1187c5
|
feat: add Tactic.Context.recover for controlling error recovery
Moreover, when executing `tac_1 <|> tac_2`, we now disable error
recovery at `tac_1`.
closes #1126 #1127
|
2022-04-27 10:47:15 -07:00 |
|
Leonardo de Moura
|
ae913efa99
|
test: collect info view issues
|
2022-04-27 09:42:18 -07:00 |
|
Sebastian Ullrich
|
829c81d677
|
fix: skip antiquotations during parser recovery
|
2022-04-27 10:41:27 +02:00 |
|
Sebastian Ullrich
|
83f331b5e2
|
parseCommand: use do
|
2022-04-27 10:41:27 +02:00 |
|
Mario Carneiro
|
f37b700e6e
|
fix: use correct number of none patterns for antiquotation splice
|
2022-04-27 09:55:27 +02:00 |
|
Leonardo de Moura
|
02d0a89229
|
chore: simpStar does not make sense for dsimp
|
2022-04-26 11:26:54 -07:00 |
|
Sebastian Ullrich
|
3d2215c93c
|
doc: clean up syntax ToC
|
2022-04-26 18:58:45 +02:00 |
|
Leonardo de Moura
|
cae59c6916
|
chore: remove staging workarounds
|
2022-04-26 08:23:43 -07:00 |
|
Leonardo de Moura
|
25053594ff
|
chore: update stage0
|
2022-04-26 08:22:25 -07:00 |
|
Leonardo de Moura
|
6af1da450e
|
feat: disable only eta for classes during TC resolution
closes #1123
|
2022-04-26 08:20:39 -07:00 |
|
Sebastian Ullrich
|
814f614369
|
fix: simp attributes and macro scopes
|
2022-04-26 10:39:02 +02:00 |
|
Leonardo de Moura
|
3cf642688b
|
fix: do not generate equation theorems while processing dsimp arguments
|
2022-04-25 18:11:32 -07:00 |
|
Leonardo de Moura
|
6bc5433b17
|
fix: add support for heterogeneous equality at processGenDiseq
|
2022-04-25 16:56:03 -07:00 |
|
Leonardo de Moura
|
4a4473ff90
|
chore: update stage0
|
2022-04-25 16:35:47 -07:00 |
|
Leonardo de Moura
|
40c8db7494
|
feat: improve argument type mismatch error position, and do not stop at application type mismatch errors
|
2022-04-25 16:30:40 -07:00 |
|
Leonardo de Moura
|
0c8a6d8977
|
feat: exists es:term,+ tactic
cc: @fgdorais
|
2022-04-25 15:35:31 -07:00 |
|
Leonardo de Moura
|
29b340aa36
|
fix: consume Expr.mdata at congr tactic
fixes #1118
|
2022-04-25 06:33:32 -07:00 |
|
Leonardo de Moura
|
3ad8dcb7ff
|
fix: nasty interaction between TC resolution and Eta for structures
See
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60constructor.60.20and.20.60Applicative.60/near/279984801
|
2022-04-24 08:19:29 -07:00 |
|
Leonardo de Moura
|
47b379e1bc
|
feat: dsimp! tactic
|
2022-04-23 18:41:04 -07:00 |
|
Leonardo de Moura
|
342a26a023
|
feat: dsimp tactic
|
2022-04-23 18:05:18 -07:00 |
|
Leonardo de Moura
|
13bcbe91cd
|
fix: regression reported at issue #1113
see issue #1113
|
2022-04-23 15:39:04 -07:00 |
|
Leonardo de Moura
|
4ab57475a0
|
chore: simplify proofs
|
2022-04-23 12:47:10 -07:00 |
|