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

7120 commits

Author SHA1 Message Date
Gabriel Ebner
220ec6e42c chore: add more decimals tests 2021-10-26 11:51:30 -07:00
Gabriel Ebner
bfc74decde feat: add info field to Syntax.node 2021-10-26 20:19:27 +02:00
Gabriel Ebner
6063c662de feat: predictable naming for notation 2021-10-26 20:19:27 +02:00
Gabriel Ebner
ce15ea98c5 feat: predictable naming for macro_rules 2021-10-26 20:19:27 +02:00
Leonardo de Moura
3d1f682144 feat: missing whnf at checkParamsAndResultType 2021-10-25 13:08:43 -07:00
Leonardo de Moura
57f02804f3 feat: use forallTelescopeReducing 
This is needed now that we allow definitions at `inductive`.
 2021-10-25 13:05:23 -07:00
Leonardo de Moura
80a73dd903 feat: basic support for definitions at inductive declarations 2021-10-25 12:44:35 -07:00
Leonardo de Moura
83cf5b20a1 fix: simpLet 
Given `let x := v; b`, `simpLet` was using an incorrect local context to simplify `v`.
 2021-10-22 16:29:00 -07:00
Leonardo de Moura
78b3b8b1e8 fix: pattern should only match if the head symbols are equal 2021-10-22 14:26:11 -07:00
Leonardo de Moura
fbdb68b669 feat: conv in conv 
Featured suggested at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Pattern.20matching.20lambda.20body.20in.20conv/near/257193307
 2021-10-22 13:53:56 -07:00
Leonardo de Moura
b4a6b4f882 fix: do not consume pretty print hints at isDefEq 
TODO: improve the solution. It is too hackish.

The issue was reported here https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.E2.9C.94.20MData.20and.20unification/near/258352713
 2021-10-20 15:58:56 -07:00
Leonardo de Moura
f01a124f18 fix: builtin attribute initialization 
The failure was triggered if a module declared (only) builtin
attributes that do not have any persistent extension associated with
them.

Fixes #726
 2021-10-20 13:55:54 -07:00
Sebastian Ullrich
2e36e362cb chore: bench: apparently make doesn't like writing to /dev/null anymore? 2021-10-20 12:44:30 +02:00
Leonardo de Moura
1bd78590e6 test: for Lean 3 nocomputable issue 
Issue reported at
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/noncomputable.20tainting/near/258174927
 2021-10-19 07:15:55 -07:00
Leonardo de Moura
b7ff5d3352 fix: make sure unused 'let'-declarations are preserved in WF 2021-10-19 06:51:54 -07:00
Leonardo de Moura
1d372ed7e3 test: well-founded recursion for unary function 2021-10-19 06:47:59 -07:00
Leonardo de Moura
67c8e76b08 fix: preserve unused let declarations 
This commit fixes reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/unused.20let.20disappears/near/257528105
 2021-10-18 17:40:15 -07:00
Leonardo de Moura
c425397b45 feat: Hashable instances for UInt8 and UInt16 2021-10-18 17:19:39 -07:00
Leonardo de Moura
e336ff5f93 feat: indentation sensitiviy for macro and elab commands 
This commit fixes issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Command.20terminator/near/257674790
 2021-10-18 17:16:09 -07:00
Leonardo de Moura
284177a80a feat: missing instances and getOp for byte/float arrays 2021-10-18 16:54:56 -07:00
Leonardo de Moura
6b2303b243 fix: bug at tryLemmaCore when numExtraArgs > 1 
Fixes bug reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Simp.20bug.20-.20produces.60application.20type.20mismatch.60/near/257711901
 2021-10-18 13:59:19 -07:00
Sebastian Ullrich
d3cf0b8098 fix: deriving Ord on parameterized types 
Fixes #732
 2021-10-18 10:08:13 +02:00
Leonardo de Moura
48a40c4d0a fix: quoteString at EmitC.lean 
Fix issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Incorrect.20escaping.20of.20.5Cr.20.3F/near/257061704
 2021-10-11 06:16:56 -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
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
fb27537b8e fix: appUnexpander name resolution 
fixes issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Scoping.20for.20delaborator.3F
 2021-10-09 08:29:26 -07:00
Gabriel Ebner
34eda689a1 fix: use eraseMacroScopes on trace classes 2021-10-08 11:13:19 -07:00
Leonardo de Moura
81729d96f9 fix: make sure Quot primitives stay in eta expanded form 
fixes #716
 2021-10-08 09:36:06 -07:00
Leonardo de Moura
15ac3c2542 test: small repro for issue #716 2021-10-08 09:36:06 -07:00
Leonardo de Moura
b742f0005f chore: fix test 2021-10-06 19:58:29 -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
85150731b7 test: put unit back, but rename it to someVal 
It is the simple and more efficient.
We just set `someVal` with the first value of `vars`.
Recall that `vars` is never empty.
 2021-10-06 18:09:06 -07:00
Leonardo de Moura
f64753c106 test: simplify ac_expr.lean 
We don't want to avoid proofs at `List.getIdx` and `Expr` when doing proofs by reflection.
The new encoding avoids that by using the fact that `vars` in
`Context` should never be empty.

To be honest, the best approach is still the old `unit`. We can just
rename it to `inhabitant` to make sure users don't assume it is the
unit of the AC operator. Then, we can just set it with the first element
of `vars` and avoid proofs at `denote`.
 2021-10-06 17:56:26 -07:00
Leonardo de Moura
079ad47f02 fix: mixed unary and non-unary functions 2021-10-06 17:33:51 -07:00
Leonardo de Moura
790a22c5df test: mutual recursion by well-founded recursion 2021-10-06 16:38:42 -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
8ec9fda6c4 fix: improve widening operator used at the ElimDeadBranches abstract interpreter 2021-10-06 12:54:07 -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
a12ade3da4 chore: fix test 2021-10-03 17:20:16 -07:00
Leonardo de Moura
42773941ed chore: fix test 2021-10-02 17:00:07 -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
Daniel Fabian
e1f591ba61 test: do no use unit in ac_expr.lean. 
It is not necessary to define a unit element for the proof to go through.
 2021-10-02 11:11:08 -07:00
Leonardo de Moura
2546a2cf7e test: add test for if-then-else issue 
The issue was reported here:
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Required.20type.20annotation.20using.20Array
 2021-09-30 22:23:22 -07:00
Leonardo de Moura
28d81ee456 fix: do not extract closed terms containing constants being defined 
It may produce crashes during initialization.
 2021-09-30 12:46:38 -07:00