Leonardo de Moura
|
df1bb458f9
|
fix(frontends/lean/pp): use group for lambda/pi
|
2016-07-26 15:44:03 -07:00 |
|
Leonardo de Moura
|
a73f813133
|
feat(frontends/lean/elaborator): remove coercion resolution
|
2016-07-26 14:49:01 -07:00 |
|
Leonardo de Moura
|
83d4436079
|
feat(frontends/lean/elaborator): remove poly case
|
2016-07-26 14:37:43 -07:00 |
|
Leonardo de Moura
|
3be217395c
|
feat(frontends/lean/elaborator): eliminator elaboration procedure first steps
|
2016-07-26 14:33:10 -07:00 |
|
Leonardo de Moura
|
c4953cac43
|
feat(frontends/lean/elaborator): only use eliminator elaboration is function is fully applied
|
2016-07-25 17:24:57 -07:00 |
|
Leonardo de Moura
|
1ed24a7237
|
feat(frontends/lean/elaborator): restrict use of 'eliminator' elaboration, approximate is_def_eq in the default function application elaborator
|
2016-07-25 16:25:54 -07:00 |
|
Leonardo de Moura
|
05a0061c09
|
feat(frontends/lean/elaborator): default elaboration for function applications
|
2016-07-25 15:50:16 -07:00 |
|
Leonardo de Moura
|
01283512a6
|
feat(frontends/lean/elaborator): add code for deciding which function application elaboration procedure should be used
|
2016-07-25 12:55:28 -07:00 |
|
Leonardo de Moura
|
3c1a1d6f1b
|
chore(frontends/lean/elaborator): style
|
2016-07-23 19:06:17 -07:00 |
|
Leonardo de Moura
|
461b5f289c
|
feat(frontends/lean/elaborator): new elaborator skeleton
|
2016-07-23 19:02:17 -07:00 |
|
Leonardo de Moura
|
212d222047
|
feat(frontends/lean): quoted names
|
2016-07-22 19:06:57 -07:00 |
|
Leonardo de Moura
|
599916c352
|
fix(frontends/lean/builtin_exprs): position information
|
2016-07-22 11:22:37 -07:00 |
|
Leonardo de Moura
|
9721757d87
|
fix(frontends/lean/builtin_exprs): position information when parsing do-notation
|
2016-07-22 11:14:33 -07:00 |
|
Leonardo de Moura
|
d8e6915366
|
fix(frontends/lean/builtin_cmds): fail if expression contain metavars
|
2016-07-19 13:22:10 -04:00 |
|
Leonardo de Moura
|
59ff0eef5c
|
feat(frontends/lean/scanner): hexadecimal numerals
|
2016-07-19 13:04:27 -04:00 |
|
Leonardo de Moura
|
492c90ed1d
|
feat(frontends/lean/scanner): hex scape in character literal
|
2016-07-19 12:38:20 -04:00 |
|
Leonardo de Moura
|
3218f91e35
|
feat(frontends/lean): add support for character literals
|
2016-07-18 14:07:10 -04:00 |
|
Leonardo de Moura
|
579f643d1d
|
refactor(library): move kabstract to tactic folder
|
2016-07-18 09:57:02 -04:00 |
|
Leonardo de Moura
|
8cfe7fdeab
|
chore(frontends/lean/token_table): remove old keywords
|
2016-07-17 14:34:01 -04:00 |
|
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 |
|