max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
9228 commits 1 branch 0 tags 5.3 GiB
Commit graph

1909 commits

Author SHA1 Message Date
Leonardo de Moura
26177995c2 feat(library/tactic): add 'generalize' tactic 2016-07-16 15:41:32 -04:00
Leonardo de Moura
fbefda9b1c feat(frontends/lean): add commands 'add_key_equivalence' and 'print key_equivalences' 2016-07-16 15:41:32 -04:00
Leonardo de Moura
f79e46a8a0 fix(frontends/lean/old_elaborator): remove "old" [intro] 2016-07-10 10:39:34 -07:00
Leonardo de Moura
f34e84dacb feat(frontends/lean/parser): cute binders 2016-07-08 07:50:58 -07:00
Sebastian Ullrich
c5a8fe02ac feat(frontends/lean): add parent classes to local context in struct definitions 
Fixes #1066
 2016-07-05 19:22:08 -07:00
Daniel Selsam
9c3b7ad979 feat(simplifier/simp_extensions): basic bookkeeping 2016-07-04 17:13:19 -07:00
Leonardo de Moura
9740515be1 chore(frontends/lean/builtin_exprs): remove '#tactic' 2016-07-02 11:15:46 +01:00
Leonardo de Moura
6cb63d5f9a feat(frontends/lean/builtin_exprs): simplify '@' and '@@' 2016-07-02 11:08:18 +01:00
Leonardo de Moura
90d920b7c9 chore(frontends/lean,library/explicit): remove dead code 2016-07-02 01:57:43 +01:00
Leonardo de Moura
97719a4c5f refactor(frontends/lean): disable '!' operator, and adjust standard library 2016-07-02 01:41:46 +01:00
Leonardo de Moura
58569b82d3 refactor(frontends/lean,library,library/tactic): move type_context_cache_helper to type_context module 2016-06-30 12:03:40 +01:00
Leonardo de Moura
1a5756661f refactor(frontends/lean,library): move scope_pos_info_provider to library 2016-06-30 10:19:35 +01:00
Leonardo de Moura
bb70fbbd48 refactor(frontends/lean): simplify elaborator_context 2016-06-29 16:56:19 +01:00
Leonardo de Moura
ccc65c6171 refactor(frontends/lean): add thread local parser_pos_provider 2016-06-29 16:09:06 +01:00
Leonardo de Moura
6234d0d830 fix(frontends/lean/decl_cmds): the function name does not need to be atomic 2016-06-29 07:55:11 +01:00
Leonardo de Moura
e433417e49 feat(frontends/lean/decl_cmds): pattern variables must be atomic 2016-06-29 07:34:36 +01:00
Leonardo de Moura
bd69aacfa8 chore(frontends/lean): remove old '#simplify' command 
We can use the new tactic framework for testing the simplifier.
 2016-06-28 11:55:02 +01:00
Leonardo de Moura
e16dbac0db feat(frontends/lean): add declare_trace command 
It allows users to define their own tracing classes.
 2016-06-28 11:45:56 +01:00
Leonardo de Moura
5d225b7056 feat(frontends/lean): 'example's don't need to be trusted 2016-06-28 10:06:15 +01:00
Leonardo de Moura
fbec9053dc feat(frontends/lean/builtin_exprs): add 'else case' for do-match notation 2016-06-27 15:28:17 +01:00
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