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

3981 commits

Author SHA1 Message Date
Leonardo de Moura
a62949c49b refactor: add type LevelMVarId (and abbreviation LMarId) 
Motivation: make sure we do not mixup metavariable ids for
expression and universe level.

cc @bollu
 2022-07-24 17:21:45 -07:00
Leonardo de Moura
e0882e098b chore: avoid stackoverflow in debug build 2022-07-24 14:47:51 -07:00
Leonardo de Moura
2c825de6a1 fix: elim_scalar_array_cases 2022-07-24 14:46:46 -07:00
Leonardo de Moura
5e877b115b feat: improve calc tactic 
> Heather suggested changing the calc tactic (not the term) such that if
the final RHS does not defeq match the goal RHS, it returns a final
inequality as a subgoal.

Closes #1342
 2022-07-24 14:30:15 -07:00
Leonardo de Moura
c46ef56ac7 perf: avoid blowup at deriving Repr 
The fix is not perfect. I just avoided inlining in some builtin `Repr` instances.
The actual problem is at `ElimDeadBranches.lean`.

Closes #1365
 2022-07-24 13:10:04 -07:00
Leonardo de Moura
5253cc6742 fix: compiler support for FloatArray.casesOn and ByteArray.casesOn 
closes #1311
 2022-07-24 12:36:08 -07:00
Leonardo de Moura
7829be9d54 fix: fixes #1333 2022-07-24 12:19:53 -07:00
Leonardo de Moura
2196a3518e perf: improve lazy_delta_reduction_step heuristic 
It addresses a performance issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/performance.20of.20equality.20with.20projections.2Fmutual/near/288083209
 2022-07-24 11:48:45 -07:00
Leonardo de Moura
6cff1f1813 fix: try to postpone by .. if expectedType? = none 
Reason: it may become `some ..` later. See issue #1359

Closes #1359
 2022-07-24 08:03:25 -07:00
Sebastian Ullrich
5160cb7b0f refactor: remove some unnecessary antiquotation kind annotations 2022-07-23 17:09:32 +02:00
Sebastian Ullrich
1f081ee6cb feat: doc comment support for unif_hint 2022-07-22 14:30:49 +02:00
Sebastian Ullrich
5d187b8beb fix: register tokens in parser quotation 2022-07-21 23:49:57 +02:00
Sebastian Ullrich
563d42f6d6 fix: make foApprox mdata-invariant 2022-07-21 14:05:47 -07:00
Andrés Goens
b36b50adb2
feat: syntax for using while condition in proofs 2022-07-21 16:57:35 +00:00
Sebastian Ullrich
c43a84ca30 fix: unsafe initialize 2022-07-20 22:37:01 +02:00
Gabriel Ebner
bffd762822 feat: improve RpcEncoding derive test 2022-07-19 22:55:42 +02:00
Gabriel Ebner
3edf22f3f5 fix: crash in binop% 2022-07-17 09:57:56 -07:00
Leonardo de Moura
94df25e99b chore: update example 2022-07-13 15:13:31 -07:00
Leonardo de Moura
d1f0db7072 fix: resumePostponed backtracking 
Note that test for issue #1200 broke.
The bug fixed by this commit was allowing the example to be elaborated
correctly :(
Initially, the type of the discriminant is not available, and
`.none (α:=α)` can only be elaborated when the expected type is of the
form `C ...`. Lean then tries to elaborate the alternatives, learn
that the discriminant should be `Option ?m`, and fails because the
patterns still have metavariables after elaboration. Before the bug
fix, `resumePostpone` was **not** restoring the metavariable context,
and the assingnment would stay there. With this information, Lean
can now elaborate `.none (α:=α)`.
Although the bug had a positive impact in this case, it produced
incorrect behavior in other examples.
The fixed example looks reasonable. Thus, we will not reopen
issue #1200
 2022-07-12 16:52:45 -07:00
Leonardo de Moura
b8ed579289 fix: fixes #1300 2022-07-12 14:08:47 -07:00
Leonardo de Moura
5bd1f7bba1 fix: special support for higher order output parameters at isDefEqArgs 
closes #1299
 2022-07-11 19:05:24 -07:00
Gabriel Ebner
a8cab84735 refactor: use computed fields for Expr 2022-07-11 14:19:41 -07:00
Gabriel Ebner
eba400543d refactor: use computed fields for Name 2022-07-11 14:19:41 -07:00
Gabriel Ebner
3176943750 refactor: use computed fields for Level 2022-07-11 14:19:41 -07:00
Gabriel Ebner
a7e8a82e89 chore: require @[computedField] attribute 2022-07-11 12:26:53 -07:00
Gabriel Ebner
243439a75c feat: support modifiers in computed fields 2022-07-11 12:26:53 -07:00
Gabriel Ebner
b1eb022027 feat: computed fields 2022-07-11 12:26:53 -07:00
Leonardo de Moura
c568f11ddf feat: use default transparency at isDefEqProofIrrel 
closes #1302
 2022-07-11 12:11:10 -07:00
Leonardo de Moura
36ebccb822 chore: fix tests 2022-07-09 15:59:44 -07:00
Leonardo de Moura
4c707d3b3c feat: use binop% to elaborate %-applications 
Motivation: make sure the behavior is consistent with other arithmetic
operators.

This commit also removes the instance
```
instance : HMod (Fin n) Nat (Fin n) where
  hMod := Fin.modn
```
because we have a coercion from `Fin n` to `Nat`.
Thus, given `a : Fin n` and `b : Nat`, `a % b` is ambiguous.
 2022-07-09 14:38:35 -07:00
Leonardo de Moura
305630cc23 fix: ElabAppArgs.finalize bug 2022-07-09 13:53:15 -07:00
Leonardo de Moura
bdaabd4e7b feat: propagate return type to for-in block 2022-07-08 17:29:30 -07:00
Leonardo de Moura
d50b33175d feat: improve forIn elaborator element type propagation 2022-07-08 16:34:42 -07:00
Leonardo de Moura
e4e0f775d6 feat: improve outParam as result type support 2022-07-08 15:29:48 -07:00
Leonardo de Moura
bf91956449 fix: add workaround for issue #1293 
This is a temporary hack until we port the C++ code to Lean.

closes #1293
 2022-07-07 23:39:35 -07:00
Leonardo de Moura
58619291e9 feat: better qualified name support in recursive definitions 2022-07-07 20:15:25 -07:00
Leonardo de Moura
db47664d4a fix: discrepancy between isDefEq and whnf for transparency mode instances 2022-07-07 15:39:58 -07:00
Leonardo de Moura
fce7697151 fix: def _root_ and dotted notation in recursive definitions 
closes #1289
 2022-07-07 07:57:51 -07:00
Sebastian Ullrich
29bdc0ceac fix: bound syntax kind at v:(ppSpace ident) etc. 2022-07-07 11:49:35 +02:00
Leonardo de Moura
0425fabf8f test: test for output parameter + coercion issue 2022-07-06 16:55:08 -07:00
Leonardo de Moura
627594b88a fix: "dot"-notation should apply default instances before failing 
See new test for motivating example.
 2022-07-05 14:27:55 -07:00
Leonardo de Moura
2b2d4245dc fix: extensible tactics bug 
See comment at `expandMacros`
 2022-07-05 13:20:22 -07:00
Leonardo de Moura
2061c9bbea chore: reduce test size 
TODO: investigate why there is a stack overflow in the CI.
I didn't manage to reproduce it on my machine.
 2022-07-04 13:58:06 -07:00
Leonardo de Moura
1999db1d7c test: add test for performance issue 
This issue has bee reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/deterministic.20timeout.20with.20structures/near/288180087
 2022-07-04 07:20:12 -07:00
Leonardo de Moura
68024b11a4 fix: simp_all bug when goal has duplicate hypotheses 2022-07-03 12:44:53 -07:00
Sebastian Ullrich
2f67295c7d feat: strengthen pp* signatures 2022-07-03 19:14:49 +02:00
Leonardo de Moura
a0fdc2d050 chore: fix tests 2022-07-02 15:57:05 -07:00
Leonardo de Moura
4568fe755c chore: fix tests 2022-07-02 15:25:06 -07:00
Leonardo de Moura
053bc889a3 feat: elaborate a[i]! and a[i]? 2022-07-02 07:29:58 -07:00
Leonardo de Moura
14260f454b feat: improve is_def_eq for projections 
It implements in the kernel the optimization in the previous commit.

This commit addresses the following issue raised on Zulip.
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/unfold.20essentially.20loops/near/288083209
 2022-06-30 17:50:44 -07:00