Reference an &mut _ binder in fstar! inside loop invariant

[mamonet]

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.

[github-actions]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.