max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
27980 commits 1 branch 0 tags 5.3 GiB
Commit graph

19031 commits

Author SHA1 Message Date
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
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
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
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
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
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
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
Leonardo de Moura
cae59c6916 chore: remove staging workarounds 2022-04-26 08:23:43 -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
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
Leonardo de Moura
ed12b62e28 fix: InfoTree was missing information for (pseudo) match patterns such as x + 1. 
This kind of pattern has to be reduced to a constructor, and the
`PatternWithRef` information was being lost in the process.
 2022-04-23 12:08:59 -07:00
Leonardo de Moura
305d8e641c chore: style 2022-04-23 10:47:53 -07:00
Sebastian Ullrich
eb7bf2b272 fix: show single final state after tactic combinator 2022-04-23 17:42:32 +02:00
Sebastian Ullrich
240c5e15e9 fix: show final goal state at end of tactic combinator 2022-04-23 17:15:32 +02:00
Leonardo de Moura
34c75fc443 feat: allow ▸ even if the expected type is not available 
see issue #1116
 2022-04-23 08:00:27 -07:00
Leonardo de Moura
36fad4bba0 fix: do not assign metavariables in the major premise type when trying K 2022-04-23 07:31:51 -07:00
Leonardo de Moura
a82abee1b2 feat: sum of monomials normal form by reflection 2022-04-22 18:51:48 -07:00
Leonardo de Moura
875bf9bf34 fix: apply dsimp at lambda binders 
This fixes another regression reported at #1113
 2022-04-22 13:10:21 -07:00
Leonardo de Moura
c13ed7c0de fix: regression reported at #1113 
See #1113
 2022-04-22 11:43:58 -07:00
Leonardo de Moura
2a2aeec085 feat: LSP semantic token for where and let rec declarations 2022-04-22 09:52:20 -07:00
Leonardo de Moura
66c82dadc9 fix: the default value for structure fields may now depend on the structure parameters 2022-04-21 17:38:19 -07:00
Leonardo de Moura
09dfd97593 chore: remove temporary workaround 2022-04-21 16:29:08 -07:00
Leonardo de Moura
d1f10a2e71 feat: apply rfl theorems at dsimp 
closes #1113
 2022-04-21 16:26:57 -07:00