Sebastian Ullrich
|
463e4a2cf3
|
refactor(library/reducible): replace ext with attribute_manager
|
2016-07-29 18:51:23 -04:00 |
|
Sebastian Ullrich
|
661fafc940
|
refactor(frontends/lean): replace different attribute classes with single scoped_ext
|
2016-07-29 18:51:23 -04:00 |
|
Leonardo de Moura
|
a64d1a77ea
|
refactor(library, frontends/lean): remove old coercion management module
|
2016-07-29 13:51:26 -07:00 |
|
Leonardo de Moura
|
7ddf1e817b
|
chore(frontends/lean): coercions are disabled by default
|
2016-07-29 13:03:23 -07:00 |
|
Daniel Selsam
|
1b7f70dde9
|
feat(simplifier): expose simp_lemmas data structure
|
2016-07-29 10:44:44 -07:00 |
|
Leonardo de Moura
|
d05e5422f9
|
refactor(frontends/lean/elaborator): snapshots
|
2016-07-29 10:36:14 -07:00 |
|
Leonardo de Moura
|
aae33e02b0
|
fix(frontends/lean/elaborator): check expected type in applications, make sure we don't accidentally unfold definitions unnecessarily
|
2016-07-28 17:30:56 -07:00 |
|
Leonardo de Moura
|
cdee8b811a
|
feat(frontends/lean/elaborator): special support for elaborating have-expressions
|
2016-07-28 16:20:53 -07:00 |
|
Leonardo de Moura
|
931251d403
|
feat(frontends/lean): remove local_context from parser
|
2016-07-28 16:19:31 -07:00 |
|
Leonardo de Moura
|
a7c8cbc548
|
feat(frontends/lean/elaborator): add hard coded coercion from bool to Prop
|
2016-07-28 15:38:22 -07:00 |
|
Leonardo de Moura
|
b5f006d229
|
feat(frontends/lean/elaborator): use expected types to disambiguate overloads
|
2016-07-28 15:32:25 -07:00 |
|
Leonardo de Moura
|
e2f14f2dc4
|
feat(frontends/lean/elaborator): use full_names when displaying ambiguous overload
|
2016-07-28 15:21:07 -07:00 |
|
Leonardo de Moura
|
f5ca3cdd68
|
refactor(frontends/lean/elaborator): simplify visit_default_app_core
|
2016-07-28 15:09:23 -07:00 |
|
Leonardo de Moura
|
dcf0244ecd
|
chore(frontends/lean/parser): remove dead code
|
2016-07-28 09:56:03 -07:00 |
|
Leonardo de Moura
|
477a137db9
|
feat(frontends/lean): remove 'using' expressions
Reason: we have include/omit commands
|
2016-07-28 09:53:27 -07:00 |
|
Leonardo de Moura
|
e6627cdfc1
|
feat(frontends/lean/parser): add new_elaborator option
|
2016-07-28 09:48:12 -07:00 |
|
Leonardo de Moura
|
ba4abed588
|
fix(frontends/lean/elaborator): better position tracking for applications
|
2016-07-27 18:52:19 -07:00 |
|
Leonardo de Moura
|
acda62d725
|
fix(frontends/lean/elaborator): preserve expected_type when annotations are used
|
2016-07-27 18:48:31 -07:00 |
|
Leonardo de Moura
|
ef2e80e635
|
refactor(library/type_context): remove dangerous 'get_cache' method
|
2016-07-27 18:32:36 -07:00 |
|
Leonardo de Moura
|
690e39b261
|
feat(frontends/lean/elaborator): add checkpoint at typed_expr
|
2016-07-27 18:08:28 -07:00 |
|
Leonardo de Moura
|
12070e589a
|
feat(frontends/lean/elaborator): elaboration procedure for recursor/eliminator applications
|
2016-07-27 17:58:18 -07:00 |
|
Leonardo de Moura
|
de9075b19d
|
chore(frontends/lean/builtin_cmds): support 'sorry' at #elab command
|
2016-07-27 17:09:36 -07:00 |
|
Leonardo de Moura
|
084f82b00b
|
feat(frontends/lean/elaborator): elaborate Pi, fix visit_lambda, improve ensure_type
|
2016-07-27 16:42:45 -07:00 |
|
Leonardo de Moura
|
3a5f6f2e64
|
feat(frontends/lean/builtin_cmds): improve output produced by #elab command, use kernel type checker to check elaboration result
|
2016-07-27 15:29:25 -07:00 |
|
Leonardo de Moura
|
7ae1a2c067
|
fix(frontends/lean/elaborator): synthesize metavariables using the context where they were declared
|
2016-07-27 15:03:17 -07:00 |
|
Leonardo de Moura
|
5b0100ef0b
|
refactor(library/lazy_abstraction): lazy ==> delayed
|
2016-07-27 13:53:17 -07:00 |
|
Leonardo de Moura
|
9477b91978
|
feat(frontends/lean/elaborator): elaborate lambdas
|
2016-07-27 11:40:30 -07:00 |
|
Leonardo de Moura
|
f8b48ac955
|
feat(frontends/lean/elaborator): support for strict implicit arguments
|
2016-07-27 10:38:59 -07:00 |
|
Leonardo de Moura
|
9a98501966
|
chore(tests/lean): fix tests output
|
2016-07-26 17:54:30 -07:00 |
|
Leonardo de Moura
|
962af9d039
|
feat(frontends/lean/elaborator): support for '_'
|
2016-07-26 17:28:41 -07:00 |
|
Leonardo de Moura
|
79efd05fa2
|
fix(frontends/lean/elaborator): overloaded applications
|
2016-07-26 17:20:57 -07:00 |
|
Leonardo de Moura
|
7a92ce38bd
|
refactor(frontends/lean): elaborator_exception ==> old_elaborator_exception
|
2016-07-26 16:24:28 -07:00 |
|
Leonardo de Moura
|
2c20a65737
|
feat(frontends/lean/elaborator): overloaded application elaboration
|
2016-07-26 15:45:36 -07:00 |
|
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 |
|