Commit 1959b7d8 authored by Arthur Correnson's avatar Arthur Correnson Committed by François Bobot
Browse files

rename test

parent 23081432
......@@ -75,9 +75,6 @@ Module Intv32.
Program Definition s0 : Interval prec emax := Intv _ _ (B754_zero false) (B754_zero true) false.
Compute (is_singleton s0).
Program Theorem is_singleton_correct :
forall (I : t) (x : float32), (is_singleton I = Some x) -> (forall y, contains I y -> x = y).
Supports Markdown
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