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
Cannot make `"my_logic_function"` transparent in `"my_pub_logic_function"` as it would call a less-visible item.
because the inner function is not pub.
This causes issues when we have internal helper functions which we don't want to be pub, but which we want to be open to aid the SMT solvers.
I therefore believe this restriction should be lifted (similar to how you in regular Rust are allowed to pub a function which internally calls a private function).
The reason this came up is that I was updating CreuSAT to current Creusot. It utilises a scheme of having private _inner predicates and logic functions which take Seqs, Ints, etc, and pub wrappers around those functions which take regular Rust types. Previously these _inners where pub, which lead to me using a mix of wrappers and wrappees which made refactoring harder, and tied implementation and proof implementation together more than desired.
The text was updated successfully, but these errors were encountered:
Currently the following:
would return the following error:
because the inner function is not
pub
.This causes issues when we have internal helper functions which we don't want to be
pub
, but which we want to beopen
to aid the SMT solvers.I therefore believe this restriction should be lifted (similar to how you in regular Rust are allowed to
pub
a function which internally calls a private function).The reason this came up is that I was updating CreuSAT to current Creusot. It utilises a scheme of having private
_inner
predicates and logic functions which takeSeq
s,Int
s, etc, andpub
wrappers around those functions which take regular Rust types. Previously these_inner
s wherepub
, which lead to me using a mix of wrappers and wrappees which made refactoring harder, and tied implementation and proof implementation together more than desired.The text was updated successfully, but these errors were encountered: