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

7806 commits

Author SHA1 Message Date
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
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
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
3c14c97195 test: add unit test for Expr lens 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
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
81a685d97c test: issue #1224 
closes #1224
 2022-06-16 18:01:09 -07:00
Leonardo de Moura
d56163bd0e refactor: resolveNamespace now return a List 2022-06-16 17:16:36 -07:00
Leonardo de Moura
8d9428261e chore: remove Fix.lean 
see #1208
 2022-06-16 15:30:47 -07:00
Sebastian Ullrich
b1e3607739 fix: match tactic with multiple LHSs 2022-06-16 15:21:46 -07:00
Sebastian Ullrich
72a5c582cf chore: Nix: ignore build messages in test capture 2022-06-16 23:33:57 +02:00
Sebastian Ullrich
6f096e0f0d chore: fix tests 2022-06-16 23:33:57 +02:00
Sebastian Ullrich
ce054fb2e7 fix: introduce semicolonOrLinebreak, replace many(1) with sepBy(1) where appropriate 2022-06-16 23:33:57 +02:00
Leonardo de Moura
989d8f04e1 chore: fix tests 2022-06-14 17:27:13 -07:00
Leonardo de Moura
3b259afaf0 chore: fix tests 2022-06-14 16:43:22 -07:00
Jakob von Raumer
d7cb93e9e4 feat: allow conv mode's arg command to access implicit arguments 2022-06-14 16:15:38 -07:00
Sebastian Ullrich
43b08239b0 fix: further conv goal state refinements 2022-06-14 11:09:47 +02:00
Leonardo de Moura
77ae79be46 chore: use let/if in do blocks 2022-06-13 17:10:14 -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
dee712ec7e chore: fix test 
Pushed the wrong file in previous commit.

see #490
 2022-06-13 14:06:56 -07:00
Leonardo de Moura
9ba5831de8 fix: _root_ prefix in declarations 
closes #490
 2022-06-13 14:03:18 -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
Wojciech Nawrocki
ff15e31e85 refactor: remove redundant theorem 2022-06-12 14:01:05 -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
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
041827bed5 chore: unused variables 2022-06-07 17:54:10 -07:00
Sebastian Ullrich
130cc8bbd5 chore: fix test 2022-06-07 16:37:45 -07:00
Sebastian Ullrich
8ffa07ab25 fix: goal state on conv => 2022-06-07 17:43:16 +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
71226243fd fix: fixes #1192 2022-06-06 18:20:45 -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
2832442e7a fix: unfold declarations tagged with [matchPattern] at reduceMatcher? even if transparency setting is not the default one 
see #1193

It fixes one of the issues exposed at the issue above.
 2022-06-06 15:53:40 -07:00
larsk21
60c8a72262 fix: unused variables linter: consider induction variables as pattern variables 2022-06-06 15:53:10 -07:00
larsk21
a9293410a2 fix: unused variables linter: ignore structure, class and inductive signatures 2022-06-06 15:53:10 -07:00
Sebastian Ullrich
143b2b49c8 fix: induction: do not register _ as binder in info tree 2022-06-06 23:05:12 +02:00
Sebastian Ullrich
ec045bfbb8 feat: $_ antiquotation pattern 2022-06-04 13:57:04 +02:00
Sebastian Ullrich
05c5dd4441 fix: unused variables linter: search fvar aliases in tactics 2022-06-03 22:37:38 +02:00