Commit graph

34 commits

Author SHA1 Message Date
Leonardo de Moura
60ab6d3bd8 feat(frontends/lean): remove feature that in declarations such as (A B : Type), forced A and B to be in the same universe
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-12 17:40:30 -07:00
Leonardo de Moura
9d4c073618 feat(frontends/lean): add option --cache
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-10 11:04:16 -07:00
Leonardo de Moura
6ca80b5000 feat(frontends/lean): add 'sorry'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-31 18:35:57 -07:00
Leonardo de Moura
864fdd37da refactor(library/aliases): aliases are from name to names
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-27 21:01:59 -07:00
Leonardo de Moura
faee08591f fix(*): make sure elaborator and type_checker use the same "rules" for treating opaque definitions
This is a big change because we have to store in constraints whether we can use the "relaxed" rules or not.
The "relaxed" case says that when type checking the value of an opaque definition we can treat other opaque definitions in the same module as transparent.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-27 12:12:54 -07:00
Leonardo de Moura
78a1670905 refactor(frontends/lean): cleanup add_delayed_theorem method
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-26 14:01:20 -07:00
Leonardo de Moura
a5b9a7b296 fix(frontends/lean/decl_cmds): support for section declarations with implicit parameters, they must be tagged with '@' when creating aliases
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-25 11:10:45 -07:00
Leonardo de Moura
ad87c0b3e1 fix(frontends/lean): race condition
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-21 09:32:13 -07:00
Leonardo de Moura
6b60db7b93 fix(frontends/lean/elaborator): bug when mixing implicit arguments and sections
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-19 09:55:34 +01:00
Leonardo de Moura
661e681ac9 feat(frontends/lean/decl_cmds): allow parameters with different types to be declared using the same 'parameters' command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-17 20:47:33 +01:00
Leonardo de Moura
2e6184a721 fix(frontends/lean): more bugs in section management
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-14 06:27:36 +01:00
Leonardo de Moura
b53e6eda58 refactor(frontends/lean): eliminate the abstract method 'family' from parser
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-14 05:44:06 +01:00
Leonardo de Moura
8167ad329f fix(frontends/lean): bug in section management
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-14 05:04:01 +01:00
Leonardo de Moura
6c442b250c refactor(frontends/lean): minor code reorg
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-14 03:47:49 +01:00
Leonardo de Moura
43fa75f7a9 fix(frontends/lean/decl_cmds): typo
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-14 03:36:06 +01:00
Leonardo de Moura
7ccb9a389c feat(frontends/lean): process theorems in parallel
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-12 22:50:57 +01:00
Leonardo de Moura
5e836092cc feat(frontends/lean): allow user to suppress proofs in theorems, and let them be inferred automatically using tactic_hints
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-08 15:08:13 -07:00
Leonardo de Moura
bd1873f6b1 feat(frontends/lean): add coercion modifier
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-07 17:48:20 -07:00
Leonardo de Moura
08465f049a feat(frontends/lean): remove [class] annotation and 'class' command, they are redundant, we only need [instance] and 'instance'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-07 16:09:30 -07:00
Leonardo de Moura
c16951aba6 fix(library/aliases): aliasing behavior
The new test '../../tests/lean/run/alias3.lean' demonstrates the issue being fixed.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-07 15:40:55 -07:00
Leonardo de Moura
e8bd267a00 fet(frontends/lean): allow coercions to sort-class in the types of variable and definitions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-06 21:54:16 -07:00
Leonardo de Moura
9a13bef4f3 fix(frontends/lean): fix (and simplify) parameter universe inference
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-06 16:56:54 -07:00
Leonardo de Moura
b3de4bb061 fix(frontends/lean/decl_cmds): modifiers should be after universe parameters
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-05 21:49:32 -07:00
Leonardo de Moura
079672f6f9 feat(frontends/lean): add 'class' and 'instances' infrastructure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-04 14:28:09 -07:00
Leonardo de Moura
bccc3df1aa chore(frontends/lean): reduce code duplication
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-30 16:52:20 -07:00
Leonardo de Moura
cb000eda13 refactor(kernel): store binder_infor in local constants
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-30 11:37:46 -07:00
Leonardo de Moura
acf8c13619 feat(kernel): add strict implicit arguments
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-25 17:50:49 -07:00
Leonardo de Moura
5b6589709c fix(frontends/lean/decl_cmds): allow binders but no type in definitions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-25 09:00:57 -07:00
Leonardo de Moura
3e7dfa6212 fix(frontends/lean): infer type of definitions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-25 08:39:14 -07:00
Leonardo de Moura
d055c4880f feat(frontends/lean): connect new elaborator to frontend
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-25 08:31:00 -07:00
Leonardo de Moura
5bd86754af feat(frontends/lean/builtin_cmds): change notation for marking implicit/cast parameter in sections
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 17:51:00 -07:00
Leonardo de Moura
39177ec10a feat(frontends/lean): flip definition modifiers position, now they must occur after the identifier
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-20 11:58:05 -07:00
Leonardo de Moura
bdab979e09 feat(frontends/lean): add inductive_cmd
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-18 16:00:59 -07:00
Leonardo de Moura
461689f758 refactor(frontends/lean/builtin_cmds): move declaration commands to new file
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-18 15:55:52 -07:00