michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
4408 commits 3 branches 0 tags 28 MiB
Commit graph

18 commits

Author SHA1 Message Date
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
01000ff7df feat(library): add typed_expr macro 
We use it to enforce that a let-variable has the expected type

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-22 11:26:06 -07:00
Leonardo de Moura
07bc0727e2 feat(frontends/lean): 'let [inline]' is the default 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-21 18:24:22 -07:00
Leonardo de Moura
2486c483cf chore(kernel/error_msgs): change type mismatch error messages, closes #33 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-07 16:18:40 -07:00
Leonardo de Moura
5f360cd8ec feat(kernel/error_msgs): improve application type mismatch error messages 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-28 07:08:12 -07:00
Leonardo de Moura
cf35c07786 fix(frontends/lean): fix 'let' annotation placement and pretty printer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-26 21:00:22 -07:00
Leonardo de Moura
a59eec39b8 feat(frontends/lean): improve 'type mismatch' error position, and annotate 'have'-expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 09:44:40 -07:00
Leonardo de Moura
5eaf04518b refactor(*): rename Bool to Prop 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-22 09:43:18 -07:00
Leonardo de Moura
43eba857cb feat(frontends/lean): add let-expr pretty printer, reduce default indentation to 2 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-09 18:47:10 -07:00
Leonardo de Moura
2ef7b9be2f feat(frontends/lean): add basic pretty printer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-09 01:12:36 -07:00
Leonardo de Moura
603dafbaf7 refactor(kernel): remove 'let'-expressions 
We simulate it in the following way:
1- An opaque 'let'-expressions (let x : t := v in b) is encoded as
      ((fun (x : t), b) v)
   We also use a macro (let-macro) to mark this pattern.
   Thus, the pretty-printer knows how to display it correctly.

2- Transparent 'let'-expressions are eagerly expanded by the parser.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-24 16:27:27 -07:00
Leonardo de Moura
873a5c8605 test(lean): add 'let' expression test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 14:11:26 -07:00
Leonardo de Moura
9f06cd553e test(lean): remove tests using Lean old syntax and kernel 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 10:38:53 -07:00
Leonardo de Moura
7726ccad28 chore(builtin): rename nat, int and real modules to Nat, Int and Real. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-01 13:52:25 -08:00
Leonardo de Moura
08718e33dc refactor(builtin): only load the kernel and natural numbers by default 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-30 13:35:37 -08:00
Leonardo de Moura
bff5a6bfb2 fix(frontends/lean/pp): make sure pp and parser are using the same precedences 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-19 12:46:14 -08:00
Leonardo de Moura
2ca30571b4 Display the input term in the output of the Check command. It is useful to see the fully elaborated term. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-08 22:55:21 -07:00
Leonardo de Moura
2459c4ae7c Add (optional) type to let declarations 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-06 10:06:26 -07:00