Leonardo de Moura
58e91559d0
feat(*): use new inductive datatype module
2018-09-06 18:09:22 -07:00
Leonardo de Moura
f335623530
feat(library/constructions/brec_on): add below and ibelow for new inductive datatype module
2018-09-05 14:46:03 -07:00
Leonardo de Moura
92c4b2ee0d
chore(library/util): minor
2018-09-05 14:46:03 -07:00
Leonardo de Moura
4964ad660f
feat(library/constructions/no_confusion): add no_confusion for new inductive datatype module
2018-09-05 10:27:49 -07:00
Leonardo de Moura
4773a3be5f
feat(library/constructions/no_confusion): add no_confusion_type for new inductive datatype module
2018-09-05 09:55:13 -07:00
Leonardo de Moura
dd03747d22
chore(kernel): univ_param vs lparam, level_param_names ==> names, and other inconsistencies
2018-09-03 13:05:42 -07:00
Sebastian Ullrich
8033649335
chore(library/util): fix doc
2018-08-01 18:44:23 -07:00
Leonardo de Moura
c0e1d05199
chore(kernel): type_checker ==> old_type_checker
2018-06-06 16:10:40 -07:00
Sebastian Ullrich
f3ca420b64
feat(frontends/lean/elaborator): hide opt/auto param types when elaborating structure field values
2018-02-28 12:49:22 +01:00
Leonardo de Moura
f8e0916c64
feat(library/tactic, frontends/lean): replace a few mk_tagged_fresh_name with mk_unused_name
2018-02-21 15:04:19 -08:00
Leonardo de Moura
cc8eb83507
refactor(library/util,util): move is_internal_name to util/
2018-02-21 15:04:19 -08:00
Sebastian Ullrich
1ee945a31f
fix(library): store and validate Lean version of .olean files
...
Fixes #1770
2018-01-23 11:14:18 -08:00
Leonardo de Moura
c5df94ed17
feat(library/tactic): add support for auto params at simp tactic
2018-01-11 16:47:22 -08:00
Leonardo de Moura
ef784ce7b8
fix(library/tactic/simp_lemmas): auto_params when adding simp lemmas
2017-12-09 09:47:39 -08:00
Leonardo de Moura
14301a7f9f
feat(library/equations_compiler/compiler): generate meta auxiliary definitions for regular (recursive) definitions
...
Motivations:
- Clear execution cost semantics for recursive functions.
- Auxiliary meta definition may assist recursive definition unfolding in the type_context object.
Next step: use meta auxiliary definition at code generation.
2017-11-01 11:58:45 -07:00
Sebastian Ullrich
46c1a1a844
refactor(frontends/lean/elaborator,kernel/error_msgs): remove duplicate code
2017-07-21 01:46:31 -07:00
Daniel Selsam
538ac8d187
feat(inductive_compiler): generate injectivity lemmas
2017-03-10 22:27:18 -08:00
Leonardo de Moura
6b3e651de7
fix(library/util): get_datatype_level should not assume inductive datatype result type is a sort
...
It may be something that is reducible to a sort.
2017-03-02 11:42:16 -08:00
Leonardo de Moura
1542cd750f
feat(library/tactic/induction_tactic): use drec in the induction tactic
...
The new test failed before this change.
2017-03-01 18:34:24 -08:00
Leonardo de Moura
d1d5428808
feat(library): add check_constants.lean validation, cleanup unused names, minor stdlib fixes
2017-02-21 10:45:31 -08:00
Leonardo de Moura
797b26f402
fix(frontends/lean/tactic_notation): trace messages in nested blocks were not being displayed in the correct place
2017-02-05 18:20:10 -08:00
Leonardo de Moura
d315e424ff
feat(library/congr_lemma, library/fun_info): make sure opt_param gadget do not confuse the simplifier, fun_info, congr_lemma, etc
...
A definition such as
def f (a : nat) (b : nat := a) (c : nat := a) :=
a + b + c
should *not* be treated as a dependent function.
2017-01-30 20:23:45 -08:00
Leonardo de Moura
a6f26f0b74
chore(library): poly_unit ==> punit
...
psum, pprod and punit are used internally.
see #1341
2017-01-30 11:54:00 -08:00
Leonardo de Moura
bf9f7560f7
feat(frontends/lean): (Type u) can't be a proposition
...
(Type u) is the old (Type (u+1))
(PType u) is the old (Type u)
Type* is the old (Type (_+1))
PType* is the old Type*
The stdlib can be compiled, but we still have > 70 broken tests
See discussion at #1341
2017-01-30 11:54:00 -08:00
Leonardo de Moura
fc00275636
fix(library/compiler/elim_recursors): it was assuming that recursive arguments occur after non recursive ones
2017-01-16 22:59:17 -08:00
Leonardo de Moura
acef1efb86
fix(frontends/lean/pp,library/equations_compiler,library/tactic/smt/congruence_closure): bug at to_char function
2017-01-11 23:44:25 -08:00
Leonardo de Moura
8a12c834ca
fix(library/tactic/smt/ematch): ematch should not use app_builder since its type_context is already in tmp_mode
2017-01-07 17:06:12 -08:00
Leonardo de Moura
5e3f26ec95
feat(library/tactic/smt/congruence_closure): propagate not_exists
2017-01-06 14:00:36 -08:00
Leonardo de Moura
316507081c
feat(library/tactic/smt): unit propagation interface
2017-01-02 10:28:26 -08:00
Leonardo de Moura
b313328cb9
feat(library/equations_compiler): int constants
2016-12-25 10:00:18 -08:00
Leonardo de Moura
3061d8b9a3
feat(library): add mk_int_val_ne_proof
2016-12-24 15:22:31 -08:00
Leonardo de Moura
d431d7274a
feat(library/tactic/congruence/congruence_closure): hard code support for ne
2016-12-23 15:37:05 -08:00
Leonardo de Moura
48cd421852
feat(library/tactic/congruence): add congruence closure basics
2016-12-21 20:46:25 -08:00
Leonardo de Moura
9aa77bfdb0
feat(library/util): add mk_nat
2016-12-06 00:16:31 -08:00
Leonardo de Moura
9d52b6607d
feat(library/tactic): use annotated_head_beta_reduce instead of head_beta_reduce in tactics
2016-11-21 15:40:12 -08:00
Leonardo de Moura
e5ba0d7733
chore(*): cleanup
2016-09-27 17:30:57 -07:00
Leonardo de Moura
d59410cc41
refactor(kernel): support only proof irrelevant mode
2016-09-27 17:18:52 -07:00
Leonardo de Moura
d0d75c0923
refactor(kernel): reduce number of configurations supported in the kernel
...
Now, eta and impredicativity are assumed to be always true.
Motivation: the rest of the system assumes eta.
Regarding impredicativity, we decided to support only the standard library.
2016-09-27 17:07:01 -07:00
Leonardo de Moura
5e5285ee67
refactor(library): rename pr1/pr2 ==> fst/snd
2016-09-21 09:48:39 -07:00
Leonardo de Moura
89f62edaf0
refactor(library): reduce dependecies on old code, simplify normalize module
2016-09-19 22:12:34 -07:00
Daniel Selsam
52f87760d8
feat(src/library/inductive_compiler): support for nested inductive types
2016-09-16 12:50:59 -07:00
Daniel Selsam
b0c5744eea
feat(inductive_compiler): support for mutually inductive types
2016-09-10 14:22:27 -07:00
Leonardo de Moura
51a338d9a1
fix(library/equations_compiler/structural_rec): support for reflexive inductive datatypes
2016-08-31 10:46:32 -07:00
Leonardo de Moura
3cc8b58433
feat(library/util): add get_constructor_rec_args
2016-08-30 20:09:41 -07:00
Daniel Selsam
4f8db64e23
refactor(simplifier): many fixes, extensions, and tests
...
fix(simplifier): missing simp rule in prop simplifier
fix(library/unfold_macros): do not look for untrusted macros when using sufficient trust level
2016-08-19 14:57:03 -07:00
Leonardo de Moura
fc4e304b27
refactor(library): move equations to equations_compiler
2016-08-11 10:08:30 -07:00
Leonardo de Moura
60c4384d09
fix(library/compiler/elim_recursors): buggy way to detect recursive arguments
2016-07-06 23:27:04 -07:00
Leonardo de Moura
8333500457
refactor(library): move try_eta to util
2016-06-17 10:29:02 -07:00
Leonardo de Moura
ef8b182fb6
feat(library/util): add get_constructor_idx
2016-05-11 13:16:40 -07:00
Leonardo de Moura
5f9120be63
feat(library/util): add get_contructor_relevant_fields
2016-05-11 13:11:37 -07:00
