Skip to content

GitLab

Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Closed
Created 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 an admin enable hashed storage. More information