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
Using a reference in fstar! macro inside loop invariant doesn't work. e.g. using a mutable reference zeta_i: &mut usize in loop invariant like the following hax_lib::loop_invariant!(|i: usize| { fstar!("v $zeta_i == v $_zeta_i + (v $i * 4)") }); throws an error. However, referencing that variable inside requires works.
The text was updated successfully, but these errors were encountered:
Using a reference in fstar! macro inside loop invariant doesn't work. e.g. using a mutable reference
zeta_i: &mut usize
in loop invariant like the followinghax_lib::loop_invariant!(|i: usize| { fstar!("v $zeta_i == v $_zeta_i + (v $i * 4)") });
throws an error. However, referencing that variable insiderequires
works.The text was updated successfully, but these errors were encountered: