Leonardo de Moura
f00e6c0a96
feat(frontends/lean): anonymous instances
...
The instance name is synthesized automatically.
2016-09-23 13:34:34 -07:00
Leonardo de Moura
973bc5f1d6
feat(frontends/lean): add notation for 'sep'
2016-09-21 16:29:59 -07:00
Leonardo de Moura
c0ff9967af
feat(frontends/lean): add basic notation for collections
2016-09-21 16:20:57 -07:00
Leonardo de Moura
5e5285ee67
refactor(library): rename pr1/pr2 ==> fst/snd
2016-09-21 09:48:39 -07:00
Sebastian Ullrich
5e3e54e208
feat(library/tactic/user_attribute): Support pure function caching for user-defined attributes
2016-09-12 10:38:48 -07:00
Leonardo de Moura
6ac64c7250
feat(library/equations_compiler/elim_match): make process_transport more robust
2016-09-11 16:21:15 -07:00
Daniel Selsam
b0c5744eea
feat(inductive_compiler): support for mutually inductive types
2016-09-10 14:22:27 -07:00
Leonardo de Moura
dcc314c109
feat(library/noncomputable): improve is_noncomputable
2016-09-08 14:02:23 -07:00
Leonardo de Moura
029766495b
feat(library/equations_compiler/util): try to improve performance of lemma generation
...
There are still performance problems. Lemma generation is fine, but the
kernel is timing out when checking the lemma. We need to provide hints
to the kernel to avoid the performance problem.
2016-09-03 13:24:44 -07:00
Leonardo de Moura
cfbffb41ef
feat(library/equations_compiler): prove equation lemmas that use if-then-else
2016-09-03 13:23:09 -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
Sebastian Ullrich
ca8be3857c
feat(library/user_attribute): add user-defined attributes and make attribute_manager environment-aware
2016-08-18 12:56:44 -07:00
Leonardo de Moura
ddc3789929
feat(frontends/lean): add run_tactic command
...
This commit also adds the tactic `add_decl`.
2016-08-18 10:56:18 -07:00
Leonardo de Moura
7059609f57
feat(library/equations_compiler): equations_compiler stub, add helper equations_editor, add preprocessing
...
The first preprocessing step packs nary functions into unary using sigma types
2016-08-14 17:02:36 -07:00
Leonardo de Moura
7bb6ccc089
refactor(library/init/meta): qexpr ==> pexpr
2016-08-05 17:04:36 -07:00
Leonardo de Moura
fafea473b8
feat(frontends/lean/elaborator): coercions to sort
2016-07-30 19:47:04 -07:00
Leonardo de Moura
a0589ce8b8
feat(frontends/lean): automatic coercions
2016-07-30 11:53:25 -07:00
Sebastian Ullrich
0ebc9eada2
chore(tactic/simplifier/simp_lemmas): replace string literals
2016-07-29 18:51:23 -04:00
Daniel Selsam
75145c29ef
refactor(library/smt): move smt files from algebra
2016-07-29 10:44:44 -07:00
Daniel Selsam
e7cee1b2cd
feat(src/library/mpq_macro): numeral macros
2016-07-29 10:44:43 -07:00
Leonardo de Moura
212d222047
feat(frontends/lean): quoted names
2016-07-22 19:06:57 -07:00
Leonardo de Moura
586baa4118
feat(library,frontends/lean): support for quoted expressions in the VM, compiler and frontend
...
TODO: invoke elaborator at tactic.to_expr
2016-06-15 16:06:39 -07:00
Leonardo de Moura
5459e9ad8a
chore(frontends/lean): remove dead code
2016-06-13 10:42:38 -07:00
Leonardo de Moura
4cbcb34817
feat(library/init): add combinators SKI
2016-06-09 14:39:20 -07:00
Leonardo de Moura
0261a81eb0
feat(frontends/lean): add '()' as notation for unit.star
2016-06-08 17:26:48 -07:00
Leonardo de Moura
165d45ac32
fix(library/compiler/erase_irrelevant): monad.return was renamed to monad.ret
2016-06-08 16:17:33 -07:00
Leonardo de Moura
924f3629ee
feat(library/vm): expose name of the C++ functions that implement builtins
2016-06-02 12:48:43 -07:00
Leonardo de Moura
a6a7daff59
refactor(library/vm): avoid constants.txt when creating bindings
2016-06-02 11:45:56 -07:00
Leonardo de Moura
6f02d30185
feat(library/vm): add basic support for C++ name objects in the VM
...
We still need to add support for the recursor
2016-06-01 13:10:24 -07:00
Leonardo de Moura
8bccfc23da
feat(library/vm): add example of C function invoking Lean closure
2016-05-31 18:45:14 -07:00
Leonardo de Moura
e89082a97e
feat(library/vm,library/init): add builtin timeit primitive for profiling
2016-05-26 12:44:49 -07:00
Leonardo de Moura
3806792866
feat(frontends/lean/builtin_cmds): use 'to_string' automatically at vm_eval if type has an instance of has_to_string
2016-05-26 11:41:53 -07:00
Leonardo de Moura
cc4b70e5e5
feat(library/vm/vm_nat): add native support for nat.to_string
2016-05-26 10:55:22 -07:00
Leonardo de Moura
bf2d2b9feb
fix(library/vm,library/compiler,frontends/lean): IO monad support
2016-05-25 13:30:43 -07:00
Leonardo de Moura
e40c54013a
feat(library/vm): add basic support for IO monad
2016-05-24 17:52:22 -07:00
Leonardo de Moura
174fba9dbd
feat(frontends/lean): add support for monadic 'do'-notation
2016-05-24 17:18:15 -07:00
Leonardo de Moura
6a9e5079c9
feat(library,frontends/lean/pp): add support for new string encoding
2016-05-24 16:20:43 -07:00
Leonardo de Moura
d7e863c3f4
feat(library/compiler/erase_irrelevant): add support for quotient types
...
and expand macros
2016-05-23 17:49:42 -07:00
Leonardo de Moura
e42972b501
feat(library/compiler/erase_irrelevant): add support for acc.rec
2016-05-23 16:31:29 -07:00
Leonardo de Moura
af1908be94
feat(frontends/lean/decl_cmds): do not generate warning for definitions that are implemented in the VM
2016-05-13 18:17:20 -07:00
Leonardo de Moura
de327c0c20
feat(library/vm/vm_nat): add builtin support for nat lt
2016-05-12 16:36:37 -07:00
Leonardo de Moura
1393238c9d
fix(library/vm/vm_nat): fix constant name
2016-05-12 15:29:14 -07:00
Leonardo de Moura
3dd7cd7403
feat(library/vm): implement nat functions in C++
2016-05-10 17:35:53 -07:00
Leonardo de Moura
50fd4eb7bd
feat(compiler/erase_irrelevant): eliminate subtype.tag, subtype.rec and subtype.elt_of
2016-05-07 16:57:26 -07:00
Leonardo de Moura
329a9723cb
feat(library): tag auxiliary no_confusion definitions
2016-05-07 15:26:49 -07:00
Leonardo de Moura
156068609f
feat(compiler/preprocess_rec): do not unfold cases_on
2016-05-03 15:42:20 -07:00
Leonardo de Moura
1924b2884c
refactor(library/tactic): remove 'append' and 'interleave' tacticals
...
Preparation for major refactoring in the tactic framework.
2016-02-24 16:02:16 -08:00
Floris van Doorn
4e2cc66061
style(*): rename is_hprop/is_hset to is_prop/is_set
2016-02-22 11:15:38 -08:00
Daniel Selsam
d521063dfb
feat(library/defeq_simplifier): new simplifier that uses only definitional equalities
2016-02-22 11:01:36 -08:00
Daniel Selsam
bb4b8da582
feat(library/unification_hint): basic handling of user-supplied unification hints
2016-02-12 11:48:51 -08:00
