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
Leonardo de Moura
f0ac477d2e
feat: add sanity checks
2021-01-01 18:31:28 -08:00
Leonardo de Moura
244b72befd
feat: simpArrow
2021-01-01 17:15:15 -08:00
Leonardo de Moura
17114cc3e8
feat: make sure kernel generates KernelException.declHasMVars instead of KernelException.other
...
... when a declaration contains metavariables.
2020-12-24 06:56:22 -08:00
Leonardo de Moura
c71eebde8c
chore: remove util/buffer.h dependency from runtime
2020-12-14 18:07:28 -08:00
Leonardo de Moura
612ef66bb4
feat: store whether inductive type is nested or not
2020-12-10 14:25:23 -08:00
Leonardo de Moura
0869f38de4
chore: update structure, class, inductive
2020-11-27 15:09:30 -08:00
Leonardo de Moura
b4012fdd71
chore: remove old comment that is not true anymore
2020-11-23 08:44:50 -08:00
Leonardo de Moura
17fb995348
feat: improve mkLevelMax'
2020-11-14 08:36:23 -08:00
Leonardo de Moura
438494ae3f
chore: fix assertion
2020-11-02 06:22:46 -08:00
Leonardo de Moura
7b5f283507
chore: remove Expr.localE constructor
...
It was used by the old frontend
2020-11-01 09:37:48 -08:00
Leonardo de Moura
de568b1268
chore: remove dead code
2020-10-28 09:33:19 -07:00
Leonardo de Moura
16f7bef88f
chore: remove old frontend leftovers
2020-10-26 09:08:07 -07:00
Leonardo de Moura
ec17fcbc1a
feat: use motive to name the kernel generated recursor
...
Motivation: users can use named arguments to provide them.
2020-10-23 05:31:28 -07:00
Sebastian Ullrich
438b3351dd
feat: add interpreter.prefer_native option
2020-10-21 11:21:56 +02:00
Sebastian Ullrich
f5565d1d92
fix: mark a few more things as persistent
2020-10-11 17:43:28 +02:00
Sebastian Ullrich
c3c037b4de
fix: fixup a few automatic fixes
2020-10-11 17:43:28 +02:00
Sebastian Ullrich
7718795178
fix: mark Lean objects in C++ globals reachable from the new frontend as persistent
...
sed -Ei 's/(g_\w+)\s*= new (name|expr|format|level|string_ref)\W.*;/\0\n mark_persistent(\1->raw());/' src/kernel/**/*.cpp src/util/**/*.cpp src/library/**/*.cpp
2020-10-11 17:43:28 +02:00
Leonardo de Moura
8383177c96
fix: nonoptimal specialization
...
@Kha Here is the fix for the problem I told you this morning.
Please, take a look at `specialize.cpp` and see whether it makes sense.
2020-09-24 12:40:28 -07:00
Leonardo de Moura
1480b39d86
chore: no Task in Theorem
2020-09-03 08:47:55 -07:00
Leonardo de Moura
b64e44fc44
fix: allow kernel projections to be used in inductive families containing only one constructor
2020-08-05 12:56:04 -07:00
Leonardo de Moura
fb5440a074
fix: new frontend does not eagerly simplify universe level expressions
...
Remark: even if we change the new frontend to simplify all universe
level expressions, we should not rely on this property in the kernel.
Reason: users may still create terms without this property.
Remark: this bug was preventing the kernel from accepting valid declarations.
2020-07-24 15:45:01 -07:00
Leonardo de Moura
d044e9f47e
chore: remove instance cache
...
If the missing cache generates perf problems in the future, we should
add the cache at `MetaM`.
cc @Kha
2020-07-08 09:40:34 -07:00
Leonardo de Moura
7c76a19885
chore: fix includes
2020-05-22 14:17:25 -07:00
