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

1745 commits

Author SHA1 Message Date
Siddharth Bhat
3374806d0f refactor: eliminate unused ExtractMonadResult.hasBindInst 2021-10-15 06:57:24 -07:00
Leonardo de Moura
002fb7f446 fix: make sure pattern is tried on partial applications 
This commit fixes issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Pattern.20matching.20lambda.20body.20in.20conv/near/256939753
 2021-10-10 15:47:04 -07:00
Leonardo de Moura
04fae18fe4 fix: make sure stop conv pattern stop at first match 2021-10-10 15:47:04 -07:00
Leonardo de Moura
e8bdb66dda fix: make sure we can match pattern inside binders 
This commit fixes issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Pattern.20matching.20lambda.20body.20in.20conv/near/256890867
 2021-10-10 15:47:04 -07:00
Leonardo de Moura
697e0ce2db feat: apply cleanup tactic before applying decreasing tactic 
Alternative design: apply it only before reporting a failure.
 2021-10-06 19:56:57 -07:00
Leonardo de Moura
c02b4f2675 refactor: move to Meta namespace 2021-10-06 19:05:37 -07:00
Leonardo de Moura
f10101cd58 fix: preserve user variable names in decreasing goals 2021-10-06 18:45:48 -07:00
Leonardo de Moura
079ad47f02 fix: mixed unary and non-unary functions 2021-10-06 17:33:51 -07:00
Leonardo de Moura
7f660af4c6 feat: add repeat tactic to conv mode 2021-10-06 14:05:44 -07:00
Leonardo de Moura
1f2e92ea04 feat: make sure #check produces some result even when there are pending TC problems 
Lean 3 uses the same approach.

closes #714
 2021-10-06 13:37:06 -07:00
Leonardo de Moura
988e43d2b4 fix: WF should reject definitions that do not take any arguments 2021-10-04 13:24:30 -07:00
Leonardo de Moura
85c49cfeb3 feat: apply termination tactic provided by user 2021-10-03 18:47:52 -07:00
Leonardo de Moura
23740778d4 refactor: termination hints 2021-10-03 18:09:35 -07:00
Leonardo de Moura
d22a42358f feat: add decreasing_tactic notation 2021-10-03 17:16:29 -07:00
Leonardo de Moura
1cdad2be46 fix: missing info trees at let_mvar% elaborator 2021-10-02 20:19:37 -07:00
Leonardo de Moura
53cee4df08 chore: typo 2021-10-02 17:45:08 -07:00
Leonardo de Moura
c24cd877c8 chore: define if-then-else again as a macro 
We can do it using the new auxiliary notation `let_mvar%` and
`wait_if_type_mvar%`.
 2021-10-02 17:30:06 -07:00
Leonardo de Moura
1e44902243 fix: add withFreshMacroScope at expandMacroImpl? 2021-10-02 16:57:25 -07:00
Leonardo de Moura
15347272c7 feat: elaborate wait_* notation 
We can use to define `if-then-else` using macros
 2021-10-02 16:27:22 -07:00
Leonardo de Moura
b510bb305d feat: elaborate let_mvar% 2021-10-02 16:12:50 -07:00
Leonardo de Moura
acd21052c0 chore: remove old notation 2021-10-02 15:06:40 -07:00
Leonardo de Moura
b99f1c698b feat: use if-then-else notation at Do.lean 
Otherwise, the `if` in the `Do` notation will not benefit from the
improved elaborator.
 2021-09-30 22:34:36 -07:00
Leonardo de Moura
eedf5b245f feat: use let_tmp at new if-then-else elaborator 2021-09-30 22:22:14 -07:00
Leonardo de Moura
35d9590b7b chore: rename let_tmp elaborator 2021-09-30 22:20:32 -07:00
Leonardo de Moura
035251d08a feat: elaborate let_zeta 2021-09-30 22:18:47 -07:00
Leonardo de Moura
cc920dd26b feat: new if-then-else elaborator that waits for condition type to be known 2021-09-30 22:07:32 -07:00
Leonardo de Moura
88c73f1daa chore: remove old if-then-else parser and elaborator 2021-09-30 20:33:58 -07:00
Leonardo de Moura
a5502e652c chore: activate builtin if-then-else elaborator 2021-09-30 20:29:49 -07:00
Leonardo de Moura
698760c5eb refactor: add if-then-else builtin parser 2021-09-30 19:33:41 -07:00
Leonardo de Moura
09d0c93589 feat: declare functions in mutual block using auxiliary fuction defined using WF 2021-09-29 11:24:52 -07:00
Leonardo de Moura
608417b946 fix: check number of explicit variables at induction/cases alternatives when @ is not used 
fixes #690
 2021-09-29 07:39:38 -07:00
Leonardo de Moura
3fed9c9df7 feat: reject partial when if constant is not a function 
fixes #697
 2021-09-28 21:07:14 -07:00
Leonardo de Moura
bd98e6a586 feat: refine WellFounded.fix functional F over PSigma.casesOn 2021-09-27 19:06:10 -07:00
Leonardo de Moura
d0391d07c2 feat: use PSigma.casesOn instead of projections at packDomain 
Reason: we want to "refine" the `WellFounded.fix` functional `F` over it.
 2021-09-27 19:06:10 -07:00
Leonardo de Moura
8b79176102 feat: refine WellFounded.fix functional F over Sum.casesOn 2021-09-27 19:06:10 -07:00
Leonardo de Moura
108518aad1 feat: use simp at mkDecreasingProof 2021-09-26 16:32:48 -07:00
Leonardo de Moura
d13bdef6e2 feat: add WF.mkFix 2021-09-26 16:01:07 -07:00
Leonardo de Moura
a7f36cc642 chore: style 2021-09-26 15:52:13 -07:00
Leonardo de Moura
9d69189a60 chore: use Sum instead of PSum at PackMutual 2021-09-25 17:24:56 -07:00
Leonardo de Moura
d4509878bb feat: add WellFoundedRelation for termination_by 2021-09-25 17:21:03 -07:00
Leonardo de Moura
ceb9889b0e feat: elaborate temination_by term 2021-09-25 16:54:41 -07:00
Leonardo de Moura
a5b27952b5 fix: panic messages on invalid input 
fixes #689
 2021-09-25 09:01:01 -07:00
Leonardo de Moura
58c938cef8 feat: 'termination_by' goodies 2021-09-22 21:09:33 -07:00
Leonardo de Moura
38f91a2fa4 doc: PackMutual.lean 2021-09-22 18:27:57 -07:00
Leonardo de Moura
0b7b174f25 feat: replace recursive applications at packMutual 2021-09-22 18:07:07 -07:00
Leonardo de Moura
b8454f3568 fix: packDomain 2021-09-22 18:00:22 -07:00
Leonardo de Moura
65983ef45b feat: add WF/PackMutual.lean 2021-09-22 15:46:47 -07:00
Sebastian Ullrich
ea244c298c chore: un-orphan file 2021-09-22 16:04:18 +02:00
Leonardo de Moura
07fb8504a1 fix: bug introduced today 2021-09-21 20:36:18 -07:00
Leonardo de Moura
a909e8cf26 feat: arity mismatch error message at well-founded recursion 2021-09-21 20:34:15 -07:00