Daniel Selsam
|
533d1ab130
|
fix(frontends/lean/inductive_cmd): remove universe placeholder from parameters
|
2016-06-14 11:36:34 -07:00 |
|
Daniel Selsam
|
a4692671e2
|
fix(src/library/defeq_simplifier): incorrect assertion
|
2016-06-14 11:31:46 -07:00 |
|
Daniel Selsam
|
6435dad371
|
fix(src/frontends/lean/builtin_cmds): typo in error message
|
2016-06-14 11:29:03 -07:00 |
|
Leonardo de Moura
|
2279807baf
|
chore(frontends/lean): remove #tactic command
|
2016-06-14 11:28:52 -07:00 |
|
Leonardo de Moura
|
179f23b64c
|
fix(library/lazy_abstraction): representation
|
2016-06-14 11:09:43 -07:00 |
|
Leonardo de Moura
|
26c10c368a
|
refactor(library): instantiate ==> instantiate_mvars
Motivation: avoid confusion with 'instantiate' procedure for variables
|
2016-06-14 10:29:47 -07:00 |
|
Leonardo de Moura
|
a16e3343a0
|
chore(library,frontends/lean): disable modules that need to be refactored
|
2016-06-14 10:02:11 -07:00 |
|
Leonardo de Moura
|
546033633b
|
feat(frontends/lean/pp): add option for pretty printing lazy-abstractions
|
2016-06-14 09:24:51 -07:00 |
|
Leonardo de Moura
|
9bcb4e05db
|
feat(library/tactic): store tactic_state at failure
|
2016-06-13 15:25:55 -07:00 |
|
Leonardo de Moura
|
6d78d0cc98
|
feat(frontends/lean/old_elaborator): interface old_elaborator with new tactic framework
The interface is not efficient, but it is sufficient for testing
purposes. We will replace the elaborator with a new one.
|
2016-06-13 13:59:01 -07:00 |
|
Leonardo de Moura
|
35022dbeca
|
feat(frontends/lean/pp): pp should not fail if infer_type fails for locals and/or metas
|
2016-06-13 12:26:41 -07:00 |
|
Leonardo de Moura
|
5459e9ad8a
|
chore(frontends/lean): remove dead code
|
2016-06-13 10:42:38 -07:00 |
|
Leonardo de Moura
|
b54203f6b3
|
feat(frontends/lean): parse by-expression
|
2016-06-13 10:25:26 -07:00 |
|
Leonardo de Moura
|
d16e1d85fb
|
chore(frontends/lean): remove proof-qed expressions
|
2016-06-13 10:04:51 -07:00 |
|
Leonardo de Moura
|
fe2b75aac7
|
fix(frontends/lean/pp,library/pp_options): 'pp.all true' should display binder types
|
2016-06-10 18:29:41 -07:00 |
|
Leonardo de Moura
|
d302514933
|
chore(frontends/lean): remove tactic notation
|
2016-06-10 18:29:41 -07:00 |
|
Leonardo de Moura
|
176afb500a
|
fix(frontends/lean/pp): make sure we are using get_local_pp_name
|
2016-06-10 18:29:40 -07:00 |
|
Leonardo de Moura
|
91204d4456
|
refactor(library/tactic/tactic_state): move tactic_state_format_expr to tactic_state module
|
2016-06-09 11:02:46 -07:00 |
|
Leonardo de Moura
|
b821a521b2
|
fix(frontends/lean/builtin_cmds): propagate options
|
2016-06-09 10:56:33 -07:00 |
|
Leonardo de Moura
|
222f7429e2
|
feat(frontends/lean/pp): pp unit.star
|
2016-06-08 17:30:11 -07:00 |
|
Leonardo de Moura
|
790980013a
|
feat(library/init/meta): add 'trace_expr'
|
2016-06-08 17:27:37 -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
|
586e9447d1
|
feat(frontends/lean/builtin_cmds): add command #tactic for testing new tactic framework
|
2016-06-08 16:19:41 -07:00 |
|
Leonardo de Moura
|
a61a6abba1
|
feat(src/frontends/lean/builtin_exprs): allow user to specify type of local decls in 'do' notation
|
2016-06-06 14:44:57 -07:00 |
|
Leonardo de Moura
|
09255e9a4c
|
fix(frontends/lean/decl_cmds): generate code for inline definitions
Reason: we only unfold inline definitions when they are fully applied.
|
2016-06-03 16:08:13 -07:00 |
|
Leonardo de Moura
|
224203f215
|
feat(library,frontends/lean/builtin_cmds): store export cmds and replay them
see #603
closes #723
|
2016-06-03 12:51:12 -07:00 |
|
Leonardo de Moura
|
0726db6e19
|
refactor(frontends/lean/builtin_cmds): separate open/export parsing from execution
|
2016-06-03 10:57:06 -07:00 |
|
Leonardo de Moura
|
f2a2207254
|
chore(frontends/lean/token_table): remove unnecessary keywords (fold and unfold)
|
2016-06-03 09:41:27 -07:00 |
|
Sebastian Ullrich
|
9561b45af1
|
fix(frontends/lean): uniform handling of declaration compound names
* allow compound names in `namespace` and `structure`
* adjust error messages
Conflicts:
src/frontends/lean/builtin_tactics.cpp
|
2016-06-02 18:13:50 -07:00 |
|
Leonardo de Moura
|
2c4935148c
|
fix(frontends/lean/decl_cmds): recursive equations for meta-definitions
|
2016-06-02 17:12:21 -07:00 |
|
Leonardo de Moura
|
df0d39ccee
|
feat(kernel,library/definitional,frontends/lean/structure_cmd): make sure we can define inductive datatypes and structures containing untrusted declarations
If they contain untrusted declarations, then the associated
declarations (e.g., constructors) will be automatically tagged as untrusted.
|
2016-06-02 16:19:06 -07:00 |
|
Sebastian Ullrich
|
647078bd40
|
feat(frontends/lean/pp): add option to hide binder types
Replace old pp.hide_binder_types option
Conflicts:
src/frontends/lean/pp.cpp
src/library/pp_options.cpp
src/library/pp_options.h
|
2016-06-02 12:01:57 -07:00 |
|
Leonardo de Moura
|
e0035f8d29
|
feat(frontends/lean/print_cmd): do not display meta constants when executing 'print axioms' cmd
|
2016-06-01 09:58:23 -07:00 |
|
Leonardo de Moura
|
5382a5a556
|
feat(frontends/lean): allow unbounded recursion in meta_definitions
|
2016-06-01 09:55:07 -07:00 |
|
Leonardo de Moura
|
e7b47a504e
|
feat(frontends/lean): add meta_definition and meta_constant commands
|
2016-06-01 09:12:41 -07:00 |
|
Leonardo de Moura
|
a2c1372d45
|
feat(frontends/lean/builtin_cmds): generate better error message when vm_eval result is a function
|
2016-05-31 19:12:02 -07:00 |
|
Leonardo de Moura
|
c9c08ab833
|
feat(frontends/lean/builtin_cmds): only display vm_eval runtime if --profile is used
|
2016-05-26 11:46:48 -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
|
53811822d4
|
chore(*): style
|
2016-05-25 18:10:15 -07:00 |
|
Leonardo de Moura
|
7c97d88be5
|
feat(frontends/lean/builtin_exprs): add optional curly braces for do-notation
|
2016-05-25 15:15:39 -07:00 |
|
Leonardo de Moura
|
76e2f92d9c
|
feat(frontends/lean/pp): pretty print let-expressions
|
2016-05-25 14:04:28 -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
|
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
|
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
|
65b9cab9b4
|
feat(frontends/lean/decl_cmds): generate bytecode when adding definitions
Remark: when the code generator fails we just generate a warning.
Reason: code generator does not support wellfounded recursion yet.
|
2016-05-13 18:05:47 -07:00 |
|
Leonardo de Moura
|
c2959dc77b
|
feat(frontends/lean/builtin_cmds): improve error message
|
2016-05-13 16:27:44 -07:00 |
|
Leonardo de Moura
|
bd23f5d63d
|
feat(frontends/lean/builtin_cmd): improve vm_eval command
|
2016-05-13 16:15:44 -07:00 |
|
Leonardo de Moura
|
dc3d7597ee
|
chore(library/vm/vm): document VM instructions
|
2016-05-13 11:54:11 -07:00 |
|
Leonardo de Moura
|
437fee1919
|
feat(frontends/lean/builtin_cmds): track runtime
|
2016-05-13 09:38:18 -07:00 |
|