Leonardo de Moura
|
6ac64c7250
|
feat(library/equations_compiler/elim_match): make process_transport more robust
|
2016-09-11 16:21:15 -07:00 |
|
Leonardo de Moura
|
4ae0ab79d9
|
feat(library/pp_options): show delayed_abstractions by default
|
2016-09-11 11:07:17 -07:00 |
|
Leonardo de Moura
|
70c7561094
|
feat(library/type_context): add more tracing messages for failures
|
2016-09-11 11:05:37 -07:00 |
|
Leonardo de Moura
|
932d14241b
|
chore(kernel): remove support for mutually inductive datatypes from the kernel
|
2016-09-10 17:39:17 -07:00 |
|
Daniel Selsam
|
5787b469d0
|
feat(inductive_compiler): a few useful helper functions
|
2016-09-10 14:22:27 -07:00 |
|
Daniel Selsam
|
b0c5744eea
|
feat(inductive_compiler): support for mutually inductive types
|
2016-09-10 14:22:27 -07:00 |
|
Leonardo de Moura
|
e6dd5242fc
|
feat(library/equations_compiler): add option eqn_compiler.zeta
|
2016-09-10 14:00:16 -07:00 |
|
Leonardo de Moura
|
1afd81384f
|
chore(library/let): delete let-macro hack
|
2016-09-10 13:06:07 -07:00 |
|
Leonardo de Moura
|
50ef0185d9
|
fix(library/equations_compiler/structural_rec): missing relaxed_whnf
|
2016-09-10 12:14:00 -07:00 |
|
Leonardo de Moura
|
96d27b6b8f
|
fix(library/equations_compiler/elim_match): missing case for is_complete_transition
|
2016-09-10 12:13:31 -07:00 |
|
Leonardo de Moura
|
b7a9174a9c
|
fix(library/type_context): never unfold constant x when solving x =?= x
This is a clean version of #1127
|
2016-09-10 09:57:38 -07:00 |
|
Leonardo de Moura
|
4df0c1fe93
|
feat(library/equations_compiler/compiler): do not use let-expresssions at pull_nested_rec_fn
|
2016-09-09 18:20:36 -07:00 |
|
Leonardo de Moura
|
532efde665
|
chore(library/local_context): fix warning
|
2016-09-09 18:01:39 -07:00 |
|
Leonardo de Moura
|
c25ac7f54f
|
feat(library/equations_compiler): pull nested recursive calls
|
2016-09-09 17:56:56 -07:00 |
|
Leonardo de Moura
|
1d5f0895d4
|
chore(library/equations_compiler/util): disable sanitizer by default
|
2016-09-09 17:53:13 -07:00 |
|
Leonardo de Moura
|
a0fb3eb2f9
|
feat(library/equations_compiler/equations): add helper function
|
2016-09-09 17:43:42 -07:00 |
|
Leonardo de Moura
|
6c13241d59
|
feat(library/local_context): add low-level methods for declaring local_decls
|
2016-09-09 17:43:07 -07:00 |
|
Leonardo de Moura
|
15f3622cbb
|
fix(library/equations_compiler/pack_domain): missing case
|
2016-09-09 13:39:51 -07:00 |
|
Leonardo de Moura
|
c1521b8416
|
feat(library/equations_compiler/elim_match): improve process_no_equation case
|
2016-09-09 12:40:16 -07:00 |
|
Leonardo de Moura
|
f64d1483e9
|
fix(library/equations_compiler/elim_match): avoid nontermination at process_no_equation
|
2016-09-09 09:00:57 -07:00 |
|
Leonardo de Moura
|
3857ae09f7
|
feat(library/equations_compiler/elim_match): add max number of steps
|
2016-09-09 08:48:34 -07:00 |
|
Daniel Selsam
|
39683fd1de
|
fix(simplifier): was calling is_def_eq on open term
|
2016-09-08 19:28:05 -07:00 |
|
Leonardo de Moura
|
b12fa5c8da
|
feat(frontends/lean): add support for 'suffices'-expression in the new elaborator
|
2016-09-08 17:26:27 -07:00 |
|
Leonardo de Moura
|
96fa8856bc
|
feat(library/equations_compiler): add mk_nonrec
|
2016-09-08 14:09:05 -07:00 |
|
Leonardo de Moura
|
dcc314c109
|
feat(library/noncomputable): improve is_noncomputable
|
2016-09-08 14:02:23 -07:00 |
|
Leonardo de Moura
|
14d009ce92
|
refactor(library/equations_compiler): improve mk_equation_lemma
|
2016-09-08 11:50:58 -07:00 |
|
Leonardo de Moura
|
f4f92ed2d1
|
chore(library/equations_compiler/util): add comment
|
2016-09-08 10:28:30 -07:00 |
|
Leonardo de Moura
|
7d56382baa
|
feat(library/equations_compiler/util): generate equation lemmas for equations using invertible functions
|
2016-09-07 17:57:10 -07:00 |
|
Leonardo de Moura
|
f7699d8719
|
fix(library/equations_compiler/elim_match): support dependent functions handling invertible functions
|
2016-09-07 16:04:08 -07:00 |
|
Leonardo de Moura
|
dd574f6a60
|
feat(library/error_handling): add display_warning
|
2016-09-07 16:03:07 -07:00 |
|
Leonardo de Moura
|
2f7a1a3579
|
feat(library/equations_compiler/elim_match): add support for invertible functions
|
2016-09-07 08:53:56 -07:00 |
|
Leonardo de Moura
|
9c8e9e07ae
|
refactor(library): injectivity ==> inverse
|
2016-09-07 08:16:14 -07:00 |
|
Leonardo de Moura
|
75155c3824
|
fix(library/tactic/cases_tactic): missing normalization
|
2016-09-06 18:46:14 -07:00 |
|
Leonardo de Moura
|
f3d2a9f1e4
|
feat(library/tactic/induction_tactic): improve error messages
|
2016-09-06 18:39:42 -07:00 |
|
Leonardo de Moura
|
89ccecc287
|
chore(library/exception): fix bad message
|
2016-09-06 18:38:39 -07:00 |
|
Leonardo de Moura
|
5e654b37d9
|
chore(library/injectivity): fix style
|
2016-09-06 18:03:16 -07:00 |
|
Leonardo de Moura
|
f954ddbdbf
|
feat(library/injectivity): add injectivity attribute
|
2016-09-06 18:01:09 -07:00 |
|
Leonardo de Moura
|
bedb508a8f
|
feat(library/equations_compiler): do not generate bytecode for lemmas
|
2016-09-06 15:14:47 -07:00 |
|
Leonardo de Moura
|
c9cee9a702
|
feat(library/equations_compiler): add flag indicating whether we are compiling a lemma or not
|
2016-09-06 15:09:54 -07:00 |
|
Leonardo de Moura
|
385a28a410
|
chore(library/equations_compiler/util): use nested_exception
|
2016-09-06 13:37:10 -07:00 |
|
Leonardo de Moura
|
01107f7aae
|
feat(library/equations_compiler): generate bytecode for auxiliary definitions
|
2016-09-06 13:29:12 -07:00 |
|
Leonardo de Moura
|
ff9500d7f9
|
feat(library/exception): add nested_exception
|
2016-09-06 12:57:06 -07:00 |
|
Leonardo de Moura
|
d8caecff49
|
refactor(library/exception): avoid throw_generic_exception functions
|
2016-09-06 12:37:56 -07:00 |
|
Leonardo de Moura
|
a0b8766ffb
|
refactor(library): merge exception modules
|
2016-09-06 09:12:26 -07:00 |
|
Leonardo de Moura
|
f354b6e430
|
chore(library/generic_exception): we will keep using generic_exception
|
2016-09-06 09:03:52 -07:00 |
|
Leonardo de Moura
|
95487f9985
|
feat(library/aux_definition): add mk_aux_lemma
|
2016-09-06 08:57:04 -07:00 |
|
Leonardo de Moura
|
2a912c2650
|
feat(frontends/lean, library): move constructor attribute to frontend
Now, it only affects the elaborator.
|
2016-09-05 09:34:45 -07:00 |
|
Leonardo de Moura
|
1cbeb071b6
|
chore(library/unifier): do not use normalizer in the old unifier
Remark: the old unifier will be deleted soon.
|
2016-09-05 08:59:15 -07:00 |
|
Leonardo de Moura
|
81a30a69d2
|
refactor(library/normalize): remove unfold and unfold_full attributes
|
2016-09-05 08:40:58 -07:00 |
|
Leonardo de Moura
|
41a958fdf4
|
chore(library/tactic/simplifier/util): warning in release mode
|
2016-09-05 08:20:59 -07:00 |
|