You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The following spec does not report any TC errors in 2.5.2:
types
ReceiptLine :: field : nat;
functions
receiptLines: () -> ReceiptLine
receiptLines() ==
let rlines = if true then [ mk_ReceiptLine(1) ] else [] in
mu(rlines(1), field |-> wibble);
However, "wibble" is undefined. The reason for this is that the conditional creation of "rlines" means that its type is "seq of ReceiptLine" or "seq of ?", and so its elements are ReceiptLine or ?. The presence of the unknown "?" is causing the mu operator to skimp on the type checking, missing the undefined variable - which should be an error, even if we don't know anything about the record type.
The text was updated successfully, but these errors were encountered:
The following spec does not report any TC errors in 2.5.2:
However, "wibble" is undefined. The reason for this is that the conditional creation of "rlines" means that its type is "seq of ReceiptLine" or "seq of ?", and so its elements are ReceiptLine or ?. The presence of the unknown "?" is causing the mu operator to skimp on the type checking, missing the undefined variable - which should be an error, even if we don't know anything about the record type.
The text was updated successfully, but these errors were encountered: