lean2/tests/lean/run/decidable.lean

import standard data.unit
using bool unit decidable

variables a b c : bool
variables u v : unit
set_option pp.implicit true
check if ((a = b) ∧ (b = c) → ¬ (u = v) ∨ (a = c) → (a = c) ↔ a = tt ↔ true) then a else b
-												fix(tests/lean): adjust tests to new library structure

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

											
										
										
											2014-08-01 09:37:23 -07:00
+								import standard data.unit
-												refactor(library/standard): rename bit to bool

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

											
										
										
											2014-07-22 09:49:54 -07:00
+								using bool unit decidable
-												feat(library/standard): add more decidable instances

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

											
										
										
											2014-07-20 01:09:37 +01:00
-												refactor(library/standard): rename bit to bool

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

											
										
										
											2014-07-22 09:49:54 -07:00
+								variables a b c : bool
-												feat(library/standard): add more decidable instances

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

											
										
										
											2014-07-20 01:09:37 +01:00
+								variables u v : unit
-												test(tests/lean/run/decidable): show implicit argument that is computed automatically

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

											
										
										
											2014-07-22 05:58:36 -07:00
+								set_option pp.implicit true
-												refactor(library/standard): use new coding style, rename bool.b0 and bool.b1 to bool.ff and bool.tt

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

											
										
										
											2014-07-28 19:58:57 -07:00
+								check if ((a = b) ∧ (b = c) → ¬ (u = v) ∨ (a = c) → (a = c) ↔ a = tt ↔ true) then a else b