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
Consider a struct X and an inherent impl block for X, as follows:
structX;implX{constA:u8 = 0;}
A is an associated constant for X.
When extracted with interface flags on to F*, this results in a let binding with a dropped_body () body.
Why this is not normal:
The current policy is that constant items that are marked "extract type-only" are actually fully translated: extracting a constant almost never yields issues, and is almost always useful in proof settings.
Plausible explanation for this bug:
Here, this policy doesn't apply probably because associated constants in inherent impls are translated with c_expr instead of c_body in thir_export.ml.
The text was updated successfully, but these errors were encountered:
Consider a struct
X
and an inherentimpl
block forX
, as follows:A
is an associated constant forX
.When extracted with interface flags on to F*, this results in a
let
binding with adropped_body ()
body.Why this is not normal:
The current policy is that constant items that are marked "extract type-only" are actually fully translated: extracting a constant almost never yields issues, and is almost always useful in proof settings.
Plausible explanation for this bug:
Here, this policy doesn't apply probably because associated constants in inherent impls are translated with
c_expr
instead ofc_body
inthir_export.ml
.The text was updated successfully, but these errors were encountered: