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

1614 commits

Author SHA1 Message Date
Gabriel Ebner
0da281fab4 fix: reject occurrences of inductive type in index 
Fixes #2125
 2023-02-28 12:22:54 -08:00
Leonardo de Moura
decb08858f fix: kernel must ensure that safe functions cannot use partial ones. 
Fix issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Meaning.20of.20.60DefinitionSafety.2Epartial.60
 2023-01-27 12:17:37 -08:00
Gabriel Ebner
34777c9b90 fix: catch missing exceptions in kernel 2023-01-23 09:27:09 -08:00
Sebastian Ullrich
a4abbf07b8 chore: remove remnants of C++ format 2022-11-18 06:11:24 -08:00
Mario Carneiro
a086d217a5 fix: bug in level normalization (soundness bug) 2022-10-26 05:22:26 -07:00
Gabriel Ebner
725aa8b39a refactor: instantiateTypeLevelParams in Lean 2022-10-24 12:23:13 -07:00
Mario Carneiro
dd8bbe9367 fix: catch kernel exceptions in Kernel.{isDefEq, whnf} 
fixes #1756
 2022-10-20 05:38:29 -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
Gabriel Ebner
c81b10f296 perf: implement Level.update* in Lean 2022-07-19 05:55:13 -07:00
Gabriel Ebner
eda3eae18e perf: implement Expr.update* in Lean 2022-07-19 05:55:13 -07:00
Gabriel Ebner
3176943750 refactor: use computed fields for Level 2022-07-11 14:19:41 -07:00
Leonardo de Moura
451abdf79d fix: Level.update* functions 
see #1291
 2022-07-10 09:16:02 -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
Leonardo de Moura
69a446c8d1 feat: add field all to DefinitionVal and TheoremVal 
Remark: we need an update stage0, and the field is not being updated
correctly set yet.
 2022-06-23 16:13:26 -07:00
Leonardo de Moura
ca6453a0ab perf: efficient unsigned hash(expr const & e) 2022-03-15 07:15:00 -07:00
Leonardo de Moura
0ef8aaeda0 feat: make sure minor premises in recursors do not include auxiliary type annotations (e.g., autoParam and optParam) 2022-03-10 08:08:36 -08:00
Leonardo de Moura
1afee372f7 refactor: move consume_type_annotations declaration to expr.h 2022-03-10 08:00:39 -08:00
Leonardo de Moura
164f07a5e5 feat: generalize Expr.abstractRange 
It now takes free variables **and** metavariables.
This is the first step to make `mkForallFVars` and `mkLambdaFVars`
more general.
 2022-03-08 18:19:17 -08:00
Leonardo de Moura
f16d8acb29 feat: eager normalization for proofs by reflection 2022-03-01 12:43:55 -08:00
Gabriel Ebner
a7c9d2735f fix: do not apply eta for structures in Prop 
The eta-expansion contains invalid projections, and the eta-rule is
subsumed by proof irrelevance anyhow.
 2022-03-01 09:00:46 -08:00
Gabriel Ebner
3746005f5f fix: reject projection (_ : ∃ x, p).2 
The inferred type of this projection does not even type check, in general.
 2022-03-01 09:00:46 -08:00
Leonardo de Moura
db38bc4043 fix: missing check at infer_proj 
We should not allow `h.1` if `h` is a proposition and the result is
not. The recursor for `h`'s type can only eliminate into `Prop`.
 2022-02-25 07:15:34 -08:00
Leonardo de Moura
f0b502aca6 fix: increase the number of heartbeats at Expr.eqv 
On issue #906, `simp` spends a lot of time checking the cache. This
process is time consuming and doesn't allocate memory. Before this
commit, it would take a long time to get the "maximum number of
heartbeats" error message on the example included in this issue.

Closes #906
 2022-01-26 08:25:33 -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
Leonardo de Moura
693a96681a doc: fix eta struct comment 2021-11-26 08:36:25 -08:00
Leonardo de Moura
0fc8c1da77 feat: eta for structures at recursors 
see #777
 2021-11-25 11:31:00 -08:00
Leonardo de Moura
50ac21d0a6 refactor: move is_constructor_app to inductive.cpp 2021-11-25 11:31:00 -08:00
Leonardo de Moura
e22bffa94f refactor: move is_structure_like to inductive.cpp 2021-11-25 11:31:00 -08:00
Leonardo de Moura
03e346bc66 chore: simplify to_cnstr_when_K 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
Leonardo de Moura
d685c545b4 feat: eta for structures 2021-11-23 06:21:25 -08:00
Leonardo de Moura
80a73dd903 feat: basic support for definitions at inductive declarations 2021-10-25 12:44:35 -07:00
Sebastian Ullrich
b13d3e6ca5 fix: dllexport functions not already annotated in header 2021-09-20 18:41:46 +02:00
Leonardo de Moura
c8406a301d chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
Leonardo de Moura
cf49e6fe8f fix: binder name 
Binder names are relevant for the `induction` tactic.
 2021-08-26 11:11:37 -07:00
Leonardo de Moura
14b611af96 refactor: move buffer.h and *_ref.h files to runtime 2021-08-16 15:39:38 -07:00
Leonardo de Moura
42561bb93f perf: change is_def_eq_proof_irrel type to lbool 2021-07-26 07:11:55 -07:00
Leonardo de Moura
8a98987e26 chore: use isDefEq heuristic on regular definitions only 2021-07-26 07:11:55 -07:00
Leonardo de Moura
3d402eda3f chore: missing ! 2021-07-23 16:04:02 -07:00
Leonardo de Moura
57b4b8ad1b chore: disable the kernel "tryHeuristic" for abbreviations 2021-07-23 12:10:16 -07:00
Sebastian Ullrich
2b451a3fed chore: remove obsolete serializer code 2021-07-22 18:59:39 +02:00
Leonardo de Moura
7424f9c8b0 chore: remove HashableUSize 2021-06-02 09:58:46 -07:00
Leonardo de Moura
cbab9438c9 chore: Hashable instances for Expr and Level 2021-06-02 08:30:25 -07:00
Wojciech Nawrocki
e5182fe4af fix: exported symbol arities 2021-05-29 07:56:54 +02:00
Leonardo de Moura
4675817a9e fix: projection of string literals 2021-05-07 14:38:21 -07:00
Leonardo de Moura
106952622a chore: modify induction hypotheses generated names 2021-05-01 16:21:12 -07:00
Leonardo de Moura
51200c916e chore: make explicit user and internal panics 2021-03-04 07:37:33 -08:00
Leonardo de Moura
023d7605fb feat: add "transitivity" to "has_loose_bvars_in_domain" 2021-02-06 17:42:38 -08:00
Leonardo de Moura
f4c9f7e163 chore: remove id_delta (aka idDelta) 
It is a leftover from Lean 3.
 2021-02-02 13:59:37 -08:00
Leonardo de Moura
ae61f2ac67 chore: remove dead code 2021-01-05 18:36:27 -08:00