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

4711 commits

Author SHA1 Message Date
Leonardo de Moura
7dbdfa090a chore: remove debugging leftovers 2022-06-13 16:37:31 -07:00
E.W.Ayers
13e286f545 doc: fix docstring for InteractiveGoal 2022-06-13 16:32:01 -07:00
E.W.Ayers
2edf02544e chore: rm ExprWithCtx 
We will make this a separate PR
 2022-06-13 16:32:01 -07:00
E.W.Ayers
367bde3601 chore: revert "refactor: replace InfoWithCtx with ExprWithCtx" 
This reverts commit db342793d53c986b8794084196552c33711f9091.
 2022-06-13 16:32:01 -07:00
E.W.Ayers
f64cb95eca refactor: replace InfoWithCtx with ExprWithCtx 
This is potentially controversial. There are still some [todo]s that need sorting.
 2022-06-13 16:32:01 -07:00
E.W.Ayers
3d561a3ab0 doc: add docstrings for interactive 2022-06-13 16:32:01 -07:00
E.W.Ayers
e3d2080232 refactor: PPExprTaggedRequest -> PPExprTaggedParams 2022-06-13 16:32:01 -07:00
E.W.Ayers
fd66e70d1e fix: explicit structure for PPExprTaggedRequest 2022-06-13 16:32:01 -07:00
E.W.Ayers
69facfbe8e fix: remove Optional from InteractiveHypothesisBundle.fvarIds 2022-06-13 16:32:01 -07:00
E.W.Ayers
45e3c72be7 refactor: InteractiveHypothesis → InteractiveHypothesisBundle 2022-06-13 16:32:01 -07:00
Ed Ayers
5130da82a8 doc: src/Lean/Widget/InteractiveGoal.lean 
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
 2022-06-13 16:32:01 -07:00
E.W.Ayers
cea53fc53e fix: tests 
Caused by a classic imperative programming bug oops
 2022-06-13 16:32:01 -07:00
E.W.Ayers
f2a874ebaa fix: handle inaccessible fvar names correctly 2022-06-13 16:32:01 -07:00
E.W.Ayers
675147dcfc fix: make InteractiveHyp.fvarIds optional 
This is for backwards compat.
 2022-06-13 16:32:01 -07:00
E.W.Ayers
0f61d1dc59 refactor: key fields are now f/mvarid fields 2022-06-13 16:32:01 -07:00
E.W.Ayers
4165b7e8ba doc: ToHide.collect 2022-06-13 16:32:01 -07:00
E.W.Ayers
6e1c9653d9 feat: Add a key field to InteractiveGoal 
This is used to uniquely identify InteractiveGoals and
InteractiveHypotheses. This makes it easier to do
contextual suggestions: eg the infoview can send a message
saying "the user clicked on subexpression 5 in hypothesis N in goal G"
where N and G are unique identifiers for a goal rather than pretty names
which may be non-unique or indices which may be difficult to compute
(eg in infoview there is a mode where hypotheses are reversed or filtered).

While adding these I also refactored the InteractiveGoal generating function.
I unwrapped a fold in to a for/in loop with mutating variables which is a
little easier to read.
 2022-06-13 16:32:01 -07:00
Wojciech Nawrocki
351be06a21 feat: ppExprTagged RPC call 2022-06-13 16:32:01 -07:00
Wojciech Nawrocki
4972f214be fix: sorried errors in rpcServerMethod 2022-06-13 16:32:01 -07:00
Leonardo de Moura
e52a7bdf42 feat: let/if indentation in do blocks 
closes #1120
 2022-06-13 16:18:49 -07:00
Leonardo de Moura
415f5f2a42 chore: style 2022-06-13 15:59:55 -07:00
Leonardo de Moura
9ba5831de8 fix: _root_ prefix in declarations 
closes #490
 2022-06-13 14:03:18 -07:00
Leonardo de Moura
328586988c chore: style 2022-06-13 13:58:29 -07:00
Leonardo de Moura
fb574af873 fix: mkSplitterProof 
This commit fixes the first issue reported at #1179

closes #1179
 2022-06-12 19:38:54 -07:00
Leonardo de Moura
09d1530d8e feat: detect unexpected occurrences of match-expression minor premises 
The error message is far from perfect, but it is better than ignoring
the issue and failing later with an even more incomprehensible error
message.

see #1179
 2022-06-12 12:07:42 -07:00
Leonardo de Moura
8a8a8b5e48 chore: style 2022-06-10 18:27:43 -07:00
Jakob von Raumer
033618ad5e fix: indices in conv arg now count arguments with forward dependencies 2022-06-10 18:25:34 -07:00
Leonardo de Moura
17db981880 fix: equation theorem for match with more than one "as" pattern 
see #1195
see #1179
 2022-06-10 18:23:13 -07:00
Leonardo de Moura
4ba7174c0c fix: universe level parameter stabilitity issue 
See comment.
 2022-06-10 14:08:08 -07:00
Sebastian Ullrich
67087ac16e fix: bad reassignment 2022-06-10 18:28:31 +02:00
Sebastian Ullrich
61232e788a fix: check types at do pattern reassignment 2022-06-10 17:31:36 +02:00
Sebastian Ullrich
8c377436f4 fix: do not report unused variables in unfinished declarations 2022-06-10 11:27:11 +02:00
Sebastian Ullrich
41dfd06e8c fix: intro/intros: do not register _ as binder in info tree 
Fixes #1204
 2022-06-09 15:23:56 +02:00
Leonardo de Moura
d0499ebf4d fix: fixes #1200 2022-06-08 10:18:05 -07:00
Leonardo de Moura
fa64c072ab feat: where declarations at instances 
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Local.20functions.20in.20instances/near/285333999
 2022-06-07 18:48:15 -07:00
Leonardo de Moura
1e59eb2290 chore: update whereStructInst 2022-06-07 18:41:43 -07:00
Leonardo de Moura
041827bed5 chore: unused variables 2022-06-07 17:54:10 -07:00
Sebastian Ullrich
f9e2a65f75 chore: further cleanup 
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
 2022-06-07 16:37:45 -07:00
Sebastian Ullrich
8eefbf5227 chore: further clean up refactored code 2022-06-07 16:37:45 -07:00
Sebastian Ullrich
897a5de6ac chore: revert some questionable signature changes 2022-06-07 16:37:45 -07:00
Sebastian Ullrich
fb2a2b3de2 fix: fixup previous commit 2022-06-07 16:37:45 -07:00
Sebastian Ullrich
ae7b895f7a refactor: unname some unused variables 2022-06-07 16:37:45 -07:00
Sebastian Ullrich
8ffa07ab25 fix: goal state on conv => 2022-06-07 17:43:16 +02:00
Sebastian Ullrich
a07e9df66e fix: use goal prefix in plain goal response 2022-06-07 17:42:09 +02:00
Leonardo de Moura
09ddf76029 feat: simp_all now uses dependent hypotheses for simplification 
However, it does not simplify them.

closes #1194
 2022-06-06 18:31:34 -07:00
Leonardo de Moura
875e71a0d7 chore: unused variables at Simp.lean 2022-06-06 18:24:10 -07:00
Leonardo de Moura
71226243fd fix: fixes #1192 2022-06-06 18:20:45 -07:00
Leonardo de Moura
0f111da64c chore: unused variables at Inductive.lean 2022-06-06 18:15:25 -07:00
Leonardo de Moura
5055855637 feat: improve default simp discharge method 
closes #1193
 2022-06-06 17:29:12 -07:00
Leonardo de Moura
3d04899e42 refactor: add unifyEq? 2022-06-06 15:53:40 -07:00