michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
lean2/tests/lean/let1.lean.expected.out

41 lines
2.3 KiB
Text
Raw Normal View History

feat(frontends/lean): add basic pretty printer Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-09 08:12:36 +00:00
[let
((λ (and_intro : ∀ (p q : Bool), p → q → (λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) p q),
[let
((λ
(and_elim_left : ∀ (p q : Bool), (λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) p q → p),
[let
((λ
(and_elim_right :
∀ (p q : Bool),
(λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) p q → q),
and_intro)
(λ (p q : Bool) (H : (λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) p q),
H q (λ (H1 : p) (H2 : q), H2)))])
(λ (p q : Bool) (H : (λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) p q),
H p (λ (H1 : p) (H2 : q), H1)))])
(λ (p q : Bool) (H1 : p) (H2 : q) (c : Bool) (H : p → q → c), H H1 H2))] :
∀ (p q : Bool),
p → q → (λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) p q
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 23:27:23 +00:00
let1.lean:17:20: error: type mismatch at application
feat(frontends/lean): add basic pretty printer Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-09 08:12:36 +00:00
(λ (and_intro : ∀ (p q : Bool), p → q → (λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) q p),
[let
((λ
(and_elim_left : ∀ (p q : Bool), (λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) p q → p),
[let
((λ
(and_elim_right :
∀ (p q : Bool),
(λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) p q → q),
and_intro)
(λ (p q : Bool) (H : (λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) p q),
H q (λ (H1 : p) (H2 : q), H2)))])
(λ (p q : Bool) (H : (λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) p q),
H p (λ (H1 : p) (H2 : q), H1)))])
(λ (p q : Bool) (H1 : p) (H2 : q) (c : Bool) (H : p → q → c), H H1 H2)
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 23:27:23 +00:00
expected type:
feat(frontends/lean): add basic pretty printer Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-09 08:12:36 +00:00
∀ (p q : Bool),
p → q → (λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) q p
test(lean): add 'let' expression test Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-16 21:11:26 +00:00
given type:
feat(frontends/lean): add basic pretty printer Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-09 08:12:36 +00:00
∀ (p q : Bool),
p → q → (∀ (c : Bool), (p → q → c) → c)
Reference in a new issue Copy permalink