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

3576 commits

Author SHA1 Message Date
Sebastian Ullrich
465913c391 fix: this must be a keyword 2021-11-29 10:06:15 -08:00
Sebastian Ullrich
531eefb7db chore: adapt syntax 2021-11-29 10:06:15 -08:00
Leonardo de Moura
0aa32d643e fix: eta struct and proof irrelevance issue 
see #777
 2021-11-27 07:15:57 -08:00
Leonardo de Moura
2d113e83f9 feat: eta struct support for unit-like datatypes 
For example, given `a b : Unit`, we have that `a` and `b` are
definitionally equal by `etaStruct`.

See #777
 2021-11-26 08:36:25 -08:00
Sebastian Ullrich
e9f7c88299 feat: record doc strings of builtin parsers & elaborators 2021-11-26 17:13:19 +01:00
Leonardo de Moura
0fc8c1da77 feat: eta for structures at recursors 
see #777
 2021-11-25 11:31:00 -08:00
Leonardo de Moura
a8f4146070 feat: support eta struct recursively 
Addresses issues raised by @gebner at #777
 2021-11-23 17:38:48 -08:00
Gabriel Ebner
7537fa7795 fix: unfold x<y in discrimination tree module 2021-11-23 07:34:51 -08:00
Leonardo de Moura
e15a656fd2 fix: remove @[reducible] annotation from Function.comp and Function.const 
closes #813
 2021-11-23 07:29:25 -08:00
Leonardo de Moura
d685c545b4 feat: eta for structures 2021-11-23 06:21:25 -08:00
Leonardo de Moura
d9b057af03 fix: fixes #793 2021-11-22 13:28:08 -08:00
Gabriel Ebner
f55649f81b fix: prefer simp lemmas with *higher* priority 2021-11-22 11:52:45 -08:00
Leonardo de Moura
2a7b33089a fix: transparency settings at simp TC check 
fixes #790
 2021-11-15 18:09:31 -08:00
Leonardo de Moura
4b2fa38cb8 fix: #check_failure command should succeed if there are stuck TC problems 2021-11-15 16:56:55 -08:00
Leonardo de Moura
9a152d2051 fix: use withSynthesize at elabStructInstance 
fixes #783
 2021-11-15 16:45:26 -08:00
Leonardo de Moura
743810b77a feat: use binrel_no_prop% to define == notation 
fixes #764
 2021-11-09 07:46:10 -08:00
Sebastian Ullrich
177d45a752 chore: fail without decreasing proof 2021-11-06 18:29:59 +01:00
Sebastian Ullrich
03551487ad chore: simplify test 2021-11-05 10:45:27 +01:00
Sebastian Ullrich
6e45685310 fix: propositions should never be considered enum types 2021-11-04 15:27:15 -07:00
Leonardo de Moura
3367501511 fix: inaccessible annotations at isDefEq issue 
Issue was reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Change.20in.20pattern.20matching.3B.20expected.20behaviour.3F/near/259059096

fixes #742
 2021-10-27 09:26:12 -07:00
Gabriel Ebner
bfc74decde feat: add info field to Syntax.node 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
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
1d372ed7e3 test: well-founded recursion for unary function 2021-10-19 06:47:59 -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
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
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
8ec9fda6c4 fix: improve widening operator used at the ElimDeadBranches abstract interpreter 2021-10-06 12:54:07 -07:00
Leonardo de Moura
85c49cfeb3 feat: apply termination tactic provided by user 2021-10-03 18:47:52 -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
837677cb4c test: doc string 2021-09-30 11:27:09 -07:00
Leonardo de Moura
ff38774b95 test: printDecls 2021-09-29 17:44:21 -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