Commit 021443e0 authored by Clément Fumex's avatar Clément Fumex
Browse files

add zeroF_is_finite axiom

parent 4fd3f75d
......@@ -640,6 +640,8 @@ theory GenericFloat
(* is_int predicate *)
predicate is_int (x:t)
axiom zeroF_is_int: is_int zeroF
(* temporary range check on int set to 2^64; TODO find the actual
max int that don't give INF with of_int for both clones *)
(* just take max *)
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