Sebastian Ullrich
|
c755aa81bd
|
fix: properly distinguish between internal and public linker flags
|
2022-05-02 13:53:52 +02:00 |
|
Sebastian Ullrich
|
2f3396e58a
|
fix: non-termination in deduplication of lexical references
|
2022-05-02 09:51:14 +02:00 |
|
Sebastian Ullrich
|
09e4c00c68
|
fix: lexical references through x := e and similar macros
|
2022-05-01 17:46:05 +02:00 |
|
Leonardo de Moura
|
109363bc7e
|
fix: closes #1132
|
2022-05-01 08:18:30 -07:00 |
|
Leonardo de Moura
|
4eb2cfec46
|
feat: make sure case' ... => tac does not use done after tac
|
2022-05-01 07:30:11 -07:00 |
|
Leonardo de Moura
|
03524305db
|
fix: findTag?
If there is an exact match, return it.
|
2022-05-01 07:30:11 -07:00 |
|
Sebastian Ullrich
|
a0678b5f6f
|
refactor: rename confusing Reference.isDeclaration field
|
2022-05-01 16:21:15 +02:00 |
|
Sebastian Ullrich
|
7512f8ab6e
|
chore: CI: pin setup-msys2
https://github.com/msys2/setup-msys2/issues/216
|
2022-05-01 11:58:58 +02:00 |
|
Sebastian Ullrich
|
952abbf16b
|
chore: remove obsolete workaround
|
2022-05-01 11:52:53 +02:00 |
|
Sebastian Ullrich
|
4174643dbd
|
perf: optimize withAntiquot parenthesizer
Doesn't look like we'll get rid of the backtracking anytime soon
|
2022-05-01 11:52:53 +02:00 |
|
Leonardo de Moura
|
fa943d3864
|
chore: update RELEASES.md
|
2022-04-29 15:59:34 -07:00 |
|
Leonardo de Moura
|
ee0414b026
|
chore: update stage0
|
2022-04-29 15:51:47 -07:00 |
|
Leonardo de Moura
|
862492778a
|
test: add deq_correct test from Zulip
|
2022-04-29 15:50:40 -07:00 |
|
Leonardo de Moura
|
cddf9ddd95
|
fix: forallAltTelescope heterogeneous equality support
|
2022-04-29 15:37:20 -07:00 |
|
Leonardo de Moura
|
c19672e99e
|
fix: basic support for the new discriminant equality encoding at split
TODO: This is a temporary fix. We can do better.
|
2022-04-29 15:29:39 -07:00 |
|
Leonardo de Moura
|
c241ef61b1
|
fix: use HEq (if needed) for encoding h : discr equalities
|
2022-04-29 15:05:48 -07:00 |
|
Leonardo de Moura
|
351f0deae9
|
feat: add mkEqHEq
|
2022-04-29 14:31:36 -07:00 |
|
Leonardo de Moura
|
941ad84ece
|
fix: getMkMatcherInputInContext
|
2022-04-29 12:44:36 -07:00 |
|
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 |
|