lean2/tests/lean/let1.lean

-- Correct version
check let bool [inline]              := Type.{0},
          and  [inline] (p q : bool) := ∀ c : bool, (p → q → c) → c,
          infixl `∧` 25             := and,
          and_intro (p q : bool) (H1 : p) (H2 : q) : p ∧ q
              := λ (c : bool) (H : p → q → c), H H1 H2,
          and_elim_left  (p q : bool) (H : p ∧ q) : p
              := H p (λ (H1 : p) (H2 : q), H1),
          and_elim_right (p q : bool) (H : p ∧ q) : q
              := H q (λ (H1 : p) (H2 : q), H2)
       in and_intro

check let bool [inline]                := Type.{0},
          and  [inline] (p q : bool)   := ∀ c : bool, (p → q → c) → c,
          infixl `∧` 25               := and,
          and_intro [fact] (p q : bool) (H1 : p) (H2 : q) : q ∧ p
              := λ (c : bool) (H : p → q → c), H H1 H2,
          and_elim_left  (p q : bool) (H : p ∧ q) : p
              := H p (λ (H1 : p) (H2 : q), H1),
          and_elim_right (p q : bool) (H : p ∧ q) : q
              := H q (λ (H1 : p) (H2 : q), H2)
       in and_intro
test(lean): add 'let' expression test Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-06-16 21:11:26 +00:00			`-- Correct version`
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			`check let bool [inline] := Type.{0},`
			`and [inline] (p q : bool) := ∀ c : bool, (p → q → c) → c,`
			infixl `∧` 25 := and,
test(lean): add 'let' expression test Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-06-16 21:11:26 +00:00			`and_intro (p q : bool) (H1 : p) (H2 : q) : p ∧ q`
			`:= λ (c : bool) (H : p → q → c), H H1 H2,`
			`and_elim_left (p q : bool) (H : p ∧ q) : p`
			`:= H p (λ (H1 : p) (H2 : q), H1),`
			`and_elim_right (p q : bool) (H : p ∧ q) : q`
			`:= H q (λ (H1 : p) (H2 : q), H2)`
			`in and_intro`

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			`check let bool [inline] := Type.{0},`
			`and [inline] (p q : bool) := ∀ c : bool, (p → q → c) → c,`
			infixl `∧` 25 := and,
			`and_intro [fact] (p q : bool) (H1 : p) (H2 : q) : 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			`:= λ (c : bool) (H : p → q → c), H H1 H2,`
			`and_elim_left (p q : bool) (H : p ∧ q) : p`
			`:= H p (λ (H1 : p) (H2 : q), H1),`
			`and_elim_right (p q : bool) (H : p ∧ q) : q`
			`:= H q (λ (H1 : p) (H2 : q), H2)`
			`in and_intro`