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

3930 commits

Author SHA1 Message Date
Leonardo de Moura
e968dfb68c feat: elaborate do notation even when expected type is not available 
see issue #1256
 2022-06-29 13:30:06 -07:00
Leonardo de Moura
a888b21bce fix: compiler bug at And.casesOn 
Fixes issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.28libc.2B.2Babi.29.20lean.3A.3Aexception.3A.20incomplete.20case/near/287839995
 2022-06-29 06:56:17 -07:00
Sebastian Ullrich
c64ac02ffc fix: declModifiers syntax kind 2022-06-28 22:35:13 +02:00
Leonardo de Moura
34dc2572f3 fix: make sure OfScientific Float instance is never unfolded during type class resolution 
This commit fixes issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/deterministic.20timeout/near/287654818

Type class resolution was diverging when trying to synthesize
```lean
 HSub (optParam Float 0.0) (optParam Float 1.0) ?m.472
```
and Lean was diverging while unfolding
```lean
 instance : OfScientific Float where
   ofScientific m s e :=
     if s then
       let s := 64 - m.log2 -- ensure we have 64 bits of mantissa left after division
       let m := (m <<< (3 * e + s)) / 5^e
       Float.ofBinaryScientific m (-4 * e - s)
     else
       Float.ofBinaryScientific (m * 5^e) e
```
was being unfolded.

Anothe potential solution for the problem above is to erase the
`optParam` annotations before performing type class resolution.
 2022-06-27 17:40:34 -07:00
Sebastian Ullrich
3a56db2812 chore: fix tests 2022-06-27 22:37:02 +02:00
Leonardo de Moura
f4e083d507 feat: dot notation and aliases 
This commit addresses the issue raised at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Namespace-based.20overloading.20does.20not.20find.20exports/near/282946185
 2022-06-27 12:42:25 -07:00
Leonardo de Moura
fc25689f21 feat: add Syntax.eraseSuffix? 2022-06-27 10:30:57 -07:00
Leonardo de Moura
3f0a9eb424 test: add test for issue #1253 
closes #1253
 2022-06-27 09:56:47 -07:00
Leonardo de Moura
220d2e3816 feat: add filterTR and [csimp] theorem 2022-06-24 06:40:38 -07:00
Leonardo de Moura
1fd2b17a92 fix: bug at addDependencies 
closes #1247
 2022-06-24 06:20:00 -07:00
Leonardo de Moura
96a72d67f2 fix: avoid unnecessary dependencies at mkMatcher 
fixes #1237
 2022-06-23 10:21:32 -07:00
Leonardo de Moura
9678be4d81 fix: store discharge depth when caching simp results 
Closes #1234
 2022-06-21 15:35:47 -07:00
Leonardo de Moura
65d24f4e39 fix: typo at LinearExpr.toExpr 
closes #1236
 2022-06-21 14:28:26 -07:00
Leonardo de Moura
986de33097 fix: fixes #1230 2022-06-20 09:58:27 -07:00
E.W.Ayers
b6f251bcd3 fix: SubExpr.Pos.toString not terminating 
fixes 1232
 2022-06-19 16:04:50 -07: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
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
81a685d97c test: issue #1224 
closes #1224
 2022-06-16 18:01:09 -07:00
Sebastian Ullrich
b1e3607739 fix: match tactic with multiple LHSs 2022-06-16 15:21:46 -07: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
Leonardo de Moura
e52a7bdf42 feat: let/if indentation in do blocks 
closes #1120
 2022-06-13 16:18:49 -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
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
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
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
Leonardo de Moura
9d6b67eae2 fix: remove check from Simp.synthesizeArgs 
Some `simp` dischargers can handle metavariables (e.g,
`assumption`). See new test.

closes #1184
 2022-06-03 07:40:30 -07:00
larsk21
cf4e106304 fix: unused variables linter review comments 
- ignore unused variables in dep arrows
- avoid negated options
- make syntax stack generation more performant
- make ignore functions more extensible
- change message severity to `warning`
 2022-06-03 13:03:52 +02:00
larsk21
393fdef972 fix: disable linters in tests 2022-06-03 13:03:52 +02:00
Leonardo de Moura
878ef3a281 feat: improve acyclic tactic 
closes #1182
 2022-06-02 15:25:14 -07:00
Leonardo de Moura
32db316166 fix: enumeration type noConfusion was not registered 
This commit fixes issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.28kernel.29.20function.20expected.20.2EnoConfusion/near/284634050
 2022-06-01 17:58:46 -07:00
Leonardo de Moura
0631c90794 feat: implement MonadLog at CoreM 2022-05-31 17:40:55 -07:00
Leonardo de Moura
5f7cc78f17 fix: remove unnecessary let-expressions when computing the motive 
fixes #1155
 2022-05-31 07:14:56 -07:00
Leonardo de Moura
9818de078b fix: fixes #1168 2022-05-30 07:24:23 -07:00
Leonardo de Moura
fb45eb4964 fix: universe polymorphic enumeration types 
Fixes issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Incorrect.20number.20of.20universe.20levels.20parameters/near/284283021
 2022-05-30 06:43:46 -07:00
Leonardo de Moura
ca6f53b407 feat: use subst_vars at builtin decreasing_tactic 2022-05-28 16:24:32 -07:00
Leonardo de Moura
40fc64480a feat: add tactic subst_vars 2022-05-28 16:19:34 -07:00
Leonardo de Moura
2c5bafcbd8 fix: dead variables at match equation hypotheses 
This commit addresses an issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Structural.20Recursion.20Problem/near/284238723
 2022-05-28 16:09:35 -07:00
Leonardo de Moura
34bbe5d12c feat: add simp theorem List.of_toArray_eq_toArray (as bs : List α) : (as.toArray = bs.toArray) = (as = bs) := by 2022-05-27 18:26:48 -07:00
Leonardo de Moura
fbd8224b4d fix: allow recursive occurrences in binder types at WF/PackDomain.lean 
fixes #1171
 2022-05-27 11:23:51 -07:00