Skip to content

GitLab

why3
why3
Closed
Opened by Guillaume Melquiond@melquionOwner

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.

To upload designs, you'll need to enable LFS and have admin enable hashed storage. More information