Open zetah11 opened 1 year ago
When the elaborator evaluates code like
let x = f 5 fun f (x: 10) : 10 = x
it generates a late init for x which immediately returns, when it really should generate a static value. This means that non-trivial bounds in range types will generate error messages in the backend for being unevaluated number expressions.
x
number
When the elaborator evaluates code like
it generates a late init for
x
which immediately returns, when it really should generate a static value. This means that non-trivial bounds in range types will generate error messages in the backend for being unevaluatednumber
expressions.