Leonardo de Moura
|
f3803c6ee4
|
refactor(frontends/lean/elaborator_context): remove io_state from elaborator_context
|
2016-06-27 06:29:54 +01:00 |
|
Leonardo de Moura
|
2ea8b26c4f
|
refactor(library/io_state): move get_global_ios to io_state module
|
2016-06-25 20:59:52 -07:00 |
|
Leonardo de Moura
|
2b35b0056a
|
chore(library/metavar_closure): remove dead code
|
2016-06-25 13:29:59 -07:00 |
|
Leonardo de Moura
|
51a449e3c4
|
chore(library): remove dead code
|
2016-06-25 13:12:24 -07:00 |
|
Leonardo de Moura
|
59f2b9e8c2
|
refactor(library/type_context): "metavar_context & m_mctx" ==> "metavar_context m_mctx"
|
2016-06-25 13:08:03 -07:00 |
|
Leonardo de Moura
|
77286e6abb
|
fix(frontends/lean): replay exported decls in imported files
|
2016-06-25 12:13:36 -07:00 |
|
Leonardo de Moura
|
c624c2d932
|
feat(frontends/lean): allow patterns in 'do' notation
|
2016-06-24 19:28:48 -07:00 |
|
Leonardo de Moura
|
51b3ddb274
|
chore(frontends/lean/decl_cmds): use 'pattern' instead of recursive equation
|
2016-06-24 16:31:06 -07:00 |
|
Leonardo de Moura
|
3a21c9127f
|
chore(frontends/lean): removed dead tokens
|
2016-06-24 16:10:18 -07:00 |
|
Leonardo de Moura
|
d604cb8b4e
|
feat(library/vm/vm): add friendly invoke method
|
2016-06-24 15:49:40 -07:00 |
|
Daniel Selsam
|
e1bc0a68e6
|
refactor(simplifier): port skeleton to new tactic framework
Conflicts:
library/init/meta/tactic.lean
src/library/tactic/tactic_state.cpp
|
2016-06-24 15:20:40 -07:00 |
|
Leonardo de Moura
|
2b43f591c9
|
fix(library/type_context): remove m_cache_owner field
This idiom creates problem if we use (even accidentally) the copy constructor.
|
2016-06-23 14:03:46 -07:00 |
|
Daniel Selsam
|
9327d85f6c
|
chore(library/defeq_simplifier): move to new module inside library/tactic
|
2016-06-22 17:18:57 -07:00 |
|
Leonardo de Moura
|
35888fae2c
|
refactor(util/list): remove coercion from T -> list<T>
|
2016-06-22 10:00:07 -07:00 |
|
Leonardo de Moura
|
9de819baaf
|
chore(library/init/monad): change precedence for >>= and >>
We are now using the same one used in Haskell.
|
2016-06-21 18:29:07 -07:00 |
|
Leonardo de Moura
|
fd08a9badf
|
refactor(library/local_context): store pp_name in local_ref's
This commit also removes the now obsolete API get_local_pp_name from abstract_type_context
|
2016-06-21 10:50:38 -07:00 |
|
Leonardo de Moura
|
16c050b66c
|
reactor(library): port fun_info_manager to new type_context (and rename module to fun_info)
|
2016-06-21 10:42:38 -07:00 |
|
Leonardo de Moura
|
0261cb95bf
|
feat(frontends/lean/old_elaborator): use type_context for failure tactic_state
|
2016-06-20 11:09:14 -07:00 |
|
Leonardo de Moura
|
149fefe480
|
chore(frontends/lean/token_table): remove 'note' keyword
|
2016-06-20 11:01:20 -07:00 |
|
Leonardo de Moura
|
46cf91c969
|
chore(frontends/lean): remove 'assert' keyword
In Lean3, `assert` was just an alias for `have`.
|
2016-06-17 14:20:26 -07:00 |
|
Leonardo de Moura
|
8333500457
|
refactor(library): move try_eta to util
|
2016-06-17 10:29:02 -07:00 |
|
Leonardo de Moura
|
f4695c4a1d
|
chore(frontends/lean): remove #defeq_simplify command
|
2016-06-17 10:16:53 -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
|
3996f9db4d
|
feat(frontends/lean): add ( token and remove token
|
2016-06-15 13:22:31 -07:00 |
|
Leonardo de Moura
|
0eb42190f0
|
fix(tests/lean): tests
|
2016-06-14 21:52:52 -07:00 |
|
Leonardo de Moura
|
6a22c0f771
|
chore(frontends/lean/old_elaborator): improve error message
|
2016-06-14 21:47:29 -07:00 |
|
Daniel Selsam
|
214e960574
|
fix(frontends/lean/elaborator): incorrect assertion
Conflicts:
src/frontends/lean/elaborator.cpp
|
2016-06-14 18:05:39 -07:00 |
|
Daniel Selsam
|
aabdabdb17
|
fix(src/frontends/lean/structure_cmd): fixes #1036
|
2016-06-14 17:52:31 -07:00 |
|
Daniel Selsam
|
4fdf608c36
|
fix(src/frontends/lean/structure_cmd): check if indices are provided
|
2016-06-14 17:52:19 -07:00 |
|
Daniel Selsam
|
aff7ceadee
|
feat(src/frontends/lean/pp): look at pp.proofs when pp-ing coercions
|
2016-06-14 11:51:34 -07:00 |
|
Daniel Selsam
|
1d6de3412d
|
fix(src/frontends/lean/pp): pp coercions that take arguments
|
2016-06-14 11:51:19 -07:00 |
|
Daniel Selsam
|
4d77f5ab2d
|
feat(src/frontends/lean/pp): option to print theorem statements instead of proof terms
Conflicts:
src/frontends/lean/pp.cpp
src/library/pp_options.cpp
|
2016-06-14 11:50:53 -07:00 |
|
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 |
|