Commit 9473d725 authored by Andrei Paskevich's avatar Andrei Paskevich

standard library: fix warnings about spurious axioms

cloned axioms are now subject to the same sanity checks
as user-written axioms, and this is probably a good thing
parent b65dd4ae
......@@ -319,7 +319,9 @@ theory BV64
clone export BV_Gen with
constant size_int = size_int,
constant max_int = max_int
constant max_int = max_int,
goal size_int_pos,
goal two_power_size_val
end
theory BV32
......@@ -328,7 +330,9 @@ theory BV32
clone export BV_Gen with
constant size_int = size_int,
constant max_int = max_int
constant max_int = max_int,
goal size_int_pos,
goal two_power_size_val
end
theory BV16
......@@ -337,7 +341,9 @@ theory BV16
clone export BV_Gen with
constant size_int = size_int,
constant max_int = max_int
constant max_int = max_int,
goal size_int_pos,
goal two_power_size_val
end
theory BV8
......@@ -346,7 +352,9 @@ theory BV8
clone export BV_Gen with
constant size_int = size_int,
constant max_int = max_int
constant max_int = max_int,
goal size_int_pos,
goal two_power_size_val
end
(** {2 Generic Converter} *)
......
......@@ -245,7 +245,8 @@ theory Single
clone export GenFloatSpecStrict with
type t = single,
constant max = max_single,
constant max_representable_integer = max_int
constant max_representable_integer = max_int,
lemma Bounded_real_no_overflow
end
......@@ -257,7 +258,8 @@ theory Double
clone export GenFloatSpecStrict with
type t = double,
constant max = max_double,
constant max_representable_integer = max_int
constant max_representable_integer = max_int,
lemma Bounded_real_no_overflow
end
......@@ -509,7 +511,7 @@ theory GenFloatSpecFull
-> is_infinite r)
/\(is_gen_zero x /\ is_gen_zero y -> is_NaN r)
/\ product_sign r x y
/\ exact r = exact x /exact y
/\ exact r = exact x /exact y
/\ model r = model x /model y
predicate of_real_exact_post (x:real) (r:t) =
......@@ -567,7 +569,8 @@ theory SingleFull
clone export GenFloatSpecFull with
type t = single,
constant max = max_single,
constant max_representable_integer = max_int
constant max_representable_integer = max_int,
lemma Bounded_real_no_overflow
end
......@@ -582,7 +585,8 @@ theory DoubleFull
clone export GenFloatSpecFull with
type t = double,
constant max = max_double,
constant max_representable_integer = max_int
constant max_representable_integer = max_int,
lemma Bounded_real_no_overflow
end
......@@ -680,7 +684,8 @@ theory SingleMultiRounding
constant max_representable_integer = max_int,
constant min_normalized = min_normalized_single,
constant eps_normalized = eps_normalized_single,
constant eta_normalized = eta_normalized_single
constant eta_normalized = eta_normalized_single,
lemma Bounded_real_no_overflow
end
......@@ -700,6 +705,7 @@ theory DoubleMultiRounding
constant max_representable_integer = max_int,
constant min_normalized = min_normalized_double,
constant eps_normalized = eps_normalized_double,
constant eta_normalized = eta_normalized_double
constant eta_normalized = eta_normalized_double,
lemma Bounded_real_no_overflow
end
......@@ -220,7 +220,9 @@ end
theory SortedInt (** sorted sequences of integers *)
use import int.Int
clone export Sorted with type t = int, predicate le = (<=)
clone export Sorted with type t = int, predicate le = (<=),
goal TotalOrder.Refl, goal TotalOrder.Trans,
goal TotalOrder.Antisymm, goal TotalOrder.Total
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