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
hax_lib::fstar! that returns unit (computationally irrelevant F* code)
fstar! in the context of a computationally irrelevant code (e.g. in a req/ens clause), that can return any type
We can't have a polymorphic fstar! accessible in any context, because we'd need to return any type, that is we'd need to panic.
For now, we would like to have a fstar_bool!, a specialized, safe version of fstar!.
We could also have an polymorphicfstar_or_default! over types T: Default, that is defined as T::default().
The text was updated successfully, but these errors were encountered:
Currently we have:
hax_lib::fstar!
that returns unit (computationally irrelevant F* code)fstar!
in the context of a computationally irrelevant code (e.g. in a req/ens clause), that can return any typeWe can't have a polymorphic
fstar!
accessible in any context, because we'd need to return any type, that is we'd need to panic.For now, we would like to have a
fstar_bool!
, a specialized, safe version offstar!
.We could also have an polymorphic
fstar_or_default!
over typesT: Default
, that is defined asT::default()
.The text was updated successfully, but these errors were encountered: