Commit 09547524 authored by François Bobot's avatar François Bobot

minmax : could we use ifthenelse instead

parent 49f961a2
......@@ -13,3 +13,10 @@ theory Test
goal SquareNonNeg : forall x : int. 0 <= x * x
goal ZeroLessOne : 0 <= 1
end
theory MinMax
use import int.MinMax
goal G : min 1 (min 3 2) = 1
end
theory Prop
logic a
logic b
goal G : a and b -> a
goal G2 : G -> true
end
\ No newline at end of file
......@@ -40,10 +40,16 @@ theory MinMax
lemma Min_sym: forall x y:t. ge x y -> min x y = min y x
(*
logic min (x y : t) : t
axiom Min_def : if ge x y then min x y = y else min x y = x
logic min (x y : t) : t
axiom Min_def : if ge x y then min x y = y else min x y = x
logic max (x y : t) : t
axiom Max_def : if ge x y then max x y = x else max x y = y
axiom Max_def : if ge x y then max x y = x else max x y = y
*)
(*
logic min (x y : t) : t = if ge x y then y else x
logic max (x y : t) : t = if ge x y then x else y
*)
end
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment