Leonardo de Moura
87592cdb43
refactor(library): remove dead code
2014-09-18 22:45:53 -07:00
Leonardo de Moura
dd31ed60b0
refactor(library): remove unnecessary file hott_kernel, HoTT and
...
standard library have been merged
2014-09-18 20:30:37 -07:00
Leonardo de Moura
243f80231a
chore(kernel): fix style and lua bindings
2014-09-17 18:30:28 -07:00
Leonardo de Moura
ea1bae0143
refactor(kernel/converter): replace extra_opaque_set with predicate
...
It gives us more flexibility.
2014-09-17 17:05:13 -07:00
Leonardo de Moura
1fbb554a16
feat(library/module): provide predicate module::is_definition
2014-09-17 16:32:00 -07:00
Leonardo de Moura
e3e2370a38
feat(frontends/lean): split 'opaque_hint' command into 'opaque' and 'transparent'
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-16 18:03:40 -07:00
Leonardo de Moura
841658ec37
feat(library/error_handling): generate valid line and column information
...
when in flycheck mode
2014-09-14 20:15:22 -07:00
Leonardo de Moura
edcbe6fe10
feat(frontends/lean): allow multiple coercions from class A to B, closes #187
...
See new tests (for examples)
tests/lean/run/coe10.lean
tests/lean/run/coe11.lean
tests/lean/run/coe9.lean
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-14 12:59:43 -07:00
Leonardo de Moura
1b6d4460e9
chore(library/coercion): cleanup
2014-09-14 12:59:43 -07:00
Leonardo de Moura
d647954f93
feat(frontends/lean/elaborator): constraints associated with 'proof-qed'
...
blocks are solved independently, closes #82
2014-09-13 10:21:10 -07:00
Leonardo de Moura
029acbd1df
feat(library/coercion): better support for coercions to function-class. closes #185
2014-09-12 13:17:20 -07:00
Leonardo de Moura
62585f1c56
fix(library/coercion): remove spurious '\n'
2014-09-12 13:08:47 -07:00
Leonardo de Moura
010ecebfea
feat(frontends/lean): add proof-qed expression
...
Remark: we still have to add support to it in the elaborator.
Right now, it is just an embellished parenthesis.
2014-09-11 18:14:49 -07:00
Leonardo de Moura
85f7132efe
feat(frontends/lean/placeholder_elaborator): perform class-instance resolution in a completely independent unifier object, it also triggers the resolution when expected type does not contain metavariables, closes #175 , closes #173 , closes #68
2014-09-11 14:49:35 -07:00
Leonardo de Moura
03902d4b45
refactor(library/unifier): add option m_discard too unifier, if m_discard == false, then unsolved flex-flex constraints are returned, the unifier also does not apply "last resource" techniques that may miss many solutions.
2014-09-11 14:49:35 -07:00
Leonardo de Moura
935ba35292
feat(library/unifier): keep normalization result when processing universe level unification constraints
2014-09-11 14:49:35 -07:00
Leonardo de Moura
c7c35becb2
feat(library/io_state): add default constructor to io_state
2014-09-11 14:49:35 -07:00
Leonardo de Moura
80fd14b39e
refactor(frontends/lean): replace collect_metavars with metavar_closure helper class
2014-09-11 14:49:35 -07:00
Leonardo de Moura
bd1bc336fb
feat(library/coercion): add simple trick for defining coercions to function-class in a convenient way, closes #31
2014-09-09 14:36:36 -07:00
Leonardo de Moura
65000fa653
feat(library/coercion): rename class to 'coercions'
2014-09-09 14:03:45 -07:00
Leonardo de Moura
ee196bbf1a
fix(frontends/lean/pp): pretty printing coercions to functions, fixes #151
2014-09-09 12:49:32 -07:00
Leonardo de Moura
187661aa6a
feat(library/unifier): consider whnf case-split on flex-rigid constraints whenever the rhs contains a local constant that is not in the lhs
2014-09-09 09:27:26 -07:00
Leonardo de Moura
a5698a55ec
fix(library/unifier): catch type error when checking is_def_eq of type incorrect expressions
2014-09-09 09:27:26 -07:00
Leonardo de Moura
fd85d4702e
refactor(library/unifier): move all_local outside of the class
2014-09-09 09:27:26 -07:00
Leonardo de Moura
ebde1bcfad
feat(library/unifier): option 'unifier.computation true' will force elaborator to always consider an extra case-split when the right-hand-side of a flex-rigid constraint is not in weak-head-normal-form
2014-09-09 09:27:26 -07:00
Leonardo de Moura
b4793df653
feat(frontends/lean): rename '[fact]' to '[visible]'
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-08 07:47:42 -07:00
Leonardo de Moura
2631979f5c
fix(library/scoped_ext): section/context should not affect namespace
2014-09-07 19:59:34 -07:00
Leonardo de Moura
bbff564a1c
feat(frontends/lean): persistent notation in sections
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-06 11:14:20 -07:00
Leonardo de Moura
6632a50015
refactor(library): add namespaces 'or', 'and' and 'iff'
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 21:25:21 -07:00
Leonardo de Moura
364bba2129
feat(frontends/lean/inductive_cmd): prefix introduction rules with the name of the inductive datatype
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 17:26:36 -07:00
Leonardo de Moura
d76218e9d1
fix(frontends/lean/elaborator): bug when elaborating expressions with multiple annotations
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 11:23:58 -07:00
Leonardo de Moura
c532dcfaac
feat(library/declaration_index): add 'a|abbreviation-name|declaration-name' entries in .ilean files
2014-09-04 09:30:25 -07:00
Leonardo de Moura
d3ec5ccac1
refactor(library/declaration_index): store declarations in a map
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 07:42:18 -07:00
Leonardo de Moura
f9a90b9920
feat(frontends/lean): add 'export' command
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-03 18:37:01 -07:00
Leonardo de Moura
5e18e6609c
feat(frontends/lean): add 'as' clause to 'open' command
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-03 17:37:02 -07:00
Leonardo de Moura
e14814d4bf
feat(frontends/lean): add '[protected]' modifier
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-03 15:01:13 -07:00
Leonardo de Moura
060093cbab
refactor(library): add type_util module, and move get_expect_num_args to it
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-03 08:40:03 -07:00
Leonardo de Moura
bbdb13172e
feat(frontends/lean/server): add 'FINDP' command
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-02 12:59:48 -07:00
Leonardo de Moura
9a4472cff5
fix(frontends/lean): wrong displayed type in proof with multiple sorry's, fixes #112
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-29 14:32:53 -07:00
Leonardo de Moura
b9489ce585
fix(frontends/let): let-expression pretty printer
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-29 10:58:27 -07:00
Leonardo de Moura
be56fcf0bd
fix(frontends/lean/pp): pretty print 'let-expressions', closes #87
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-28 18:20:58 -07:00
Leonardo de Moura
b9628842cf
feat(library/unifier): remove mk_macro_imitation, we instead expand the macro before solving flex-rigid constraints
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-28 17:34:03 -07:00
Leonardo de Moura
1e80a9dfe9
feat(frontends/lean): avoid exponential blowup when processing let-expressions with a lot of sharing, cleanup show-expression
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-28 16:27:52 -07:00
Leonardo de Moura
641624a277
fix(library/unifier): bug in expand_rhs
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-28 14:35:11 -07:00
Leonardo de Moura
e303651dee
refactor(library/unifier): cleanup mk_macro_imitation
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-28 13:19:19 -07:00
Leonardo de Moura
c7e9e238ec
fix(frontends/lean/server): ignore output produced by worker thread, fixes #98
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-27 10:46:49 -07:00
Leonardo de Moura
fab4eb0d69
feat(frontends/lean/server): add CLEAR_CACHE command, closes #100
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-27 10:31:01 -07:00
Leonardo de Moura
4c9723e5ed
fix(library/unifier): assertion violation
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-26 09:07:34 -07:00
Leonardo de Moura
02b7f980b0
fix(library/num): bug in to_pos_num, missing test
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-26 08:18:07 -07:00
Leonardo de Moura
fbf13994d8
refactor(*): use + for concatenating format objects
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-24 09:35:25 -07:00