Isabelle printer: bad printing of floating-point literals
The following example
use ieee_float.Float32
let f (x: Float32.t) : Float32.t
requires { lt (0.0:t) x /\ lt x (1000.0:t) }
ensures { not (eq (add RNE x x) result) }
= mul RNE x (2.0:Float32.t)
when translated to Isabelle generated the error below. There is certainly missing something in the translation of floating-point literals.
Type unification failed: Clash of types "real" and "t"
Type error in application: incompatible operand type
Operator: lt :: t ⇒ t ⇒ bool
Operand: 0 :: real
Coercion Inference:
Local coercion insertion on the operand failed:
"real" is not a subtype of "t"
Now trying to infer coercions globally.
Coercion inference failed:
"real" is not a subtype of "t"