Confusing error message for floating-point literals
theory T
use ieee_float.Float32 as B32
goal g : (1.:B32.t) = (1:B32.t)
end
gives Type t cannot be used for a numeric literal
, which is wrong by definition.
Either the error message should be Invalid floating point literal: '1'
, or the code should just be modified to accept such a literal.