Leonardo de Moura
|
546f9dc00b
|
chore(frontends/lean): use consistent name conventions, rename token_set to token_table
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-06-10 09:18:57 -07:00 |
|
Leonardo de Moura
|
d10d70423a
|
feat(frontends/lean): add new scanner
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-06-05 18:57:26 -07:00 |
|
Leonardo de Moura
|
c6af56260e
|
refactor(frontends/lean): remove dead code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-05-15 15:51:41 -07:00 |
|
Leonardo de Moura
|
a2d2e36f04
|
refactor(frontends/lean): remove notation for creating tuples
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-02-10 09:03:42 -08:00 |
|
Leonardo de Moura
|
ad7b13104f
|
feat(*): add support for heterogeneous equality in the parser, elaborator and simplifier, adjusts unit test to reflect changes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-02-07 15:03:16 -08:00 |
|
Leonardo de Moura
|
ba9a8f9d98
|
feat(frontends/lean): add 'show' expression syntax sugar
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-02-06 07:50:22 -08:00 |
|
Leonardo de Moura
|
4fcc292332
|
feat(frontends/lean): parse and pretty print pair/tuple projection operators proj1 and proj2, fix bug in the type checker
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-02-03 22:10:01 -08:00 |
|
Leonardo de Moura
|
5e5ab1429d
|
feat(frontends/lean): parse and pretty print sigma types
This commit also fixes some bugs in the implementation of Sigma types.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-02-03 18:16:00 -08:00 |
|
Leonardo de Moura
|
f7c7dd4ed4
|
feat(frontends/lean): include filename in error messages, use GNU error message style
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-01-09 11:01:27 -08:00 |
|
Leonardo de Moura
|
048151487e
|
feat(kernel): use Pi as forall/implication
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-01-08 00:38:39 -08:00 |
|
Leonardo de Moura
|
c7338a8eab
|
chore(frontends/lean/scanner): remove dead code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-01-07 14:37:28 -08:00 |
|
Leonardo de Moura
|
6569b07b7c
|
feat(frontends/lean/parser): rename 'show' expression to 'have'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-01-05 11:25:58 -08:00 |
|
Leonardo de Moura
|
028a9bd9bd
|
feat(frontends/lean/scanner): use Lua style comments in Lean
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-01-05 08:53:27 -08:00 |
|
Leonardo de Moura
|
111949b9be
|
feat(frontends/lean): calculational proofs
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-01-02 10:53:14 -08:00 |
|
Leonardo de Moura
|
c3bc6afb12
|
refactor(library/arith): move int and nat declarations to .lean files.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-12-30 10:32:14 -08:00 |
|
Leonardo de Moura
|
1df9d18891
|
feat(frontends/lean): allow 'tactic hints' to be associated with 'holes'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-12-06 14:49:39 -08:00 |
|
Leonardo de Moura
|
57b9657bf0
|
feat(lua): add lua_exception for wrapping lua errors, and improve Lua error messages in the Lean frontend
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-11-07 15:19:26 -08:00 |
|
Leonardo de Moura
|
a9b2be0b9c
|
feat(frontends/lean): add support for embedded Lua scripts in Lean files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-11-07 13:56:04 -08:00 |
|
Soonho Kong
|
5c3866cd71
|
Use fullpath in #include directives, add missing STL headers
|
2013-09-13 03:35:29 -07:00 |
|
Leonardo de Moura
|
4c19cc6957
|
Rename lean frontend files. The prefix lean_ is not necessary anymore.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-12 20:09:35 -07:00 |
|