lean2/tests/lean/tst12.lean.expected.out

  Set: pp::colors
  Set: pp::unicode
λ x y : Bool, x ∧ y
let x := ⊤,
    y := ⊤,
    z := x ∧ y,
    f := λ arg1 arg2 : Bool, arg1 ∧ arg2 = arg2 ∧ arg1 = arg1 ∨ arg2 ∨ arg2
in f x y ∨ z
(⊤ ∧ ⊤ = ⊤ ∧ ⊤ = ⊤ ∨ ⊤ ∨ ⊤) ∨ ⊤ ∧ ⊤
-												Modify verbose message for Set command

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2013-09-02 12:29:21 -07:00
+								  Set: pp::colors
-												Fix unit tests for Windows

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2013-09-03 10:44:51 -07:00
+								  Set: pp::unicode
-												Minimize use the colors in tests. The colors make the diff hard to read

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2013-09-01 10:34:57 -07:00
+								λ x y : Bool, x ∧ y
 								let x := ⊤,
 								    y := ⊤,
 								    z := x ∧ y,
-												feat(kernel): use Pi as forall/implication

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-01-08 00:38:39 -08:00
+								    f := λ arg1 arg2 : Bool, arg1 ∧ arg2 = arg2 ∧ arg1 = arg1 ∨ arg2 ∨ arg2
-												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
+								in f x y ∨ z
-												refactor(kernel): remove semantic attachments from the kernel

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-02-01 18:27:14 -08:00
+								(⊤ ∧ ⊤ = ⊤ ∧ ⊤ = ⊤ ∨ ⊤ ∨ ⊤) ∨ ⊤ ∧ ⊤