Hi! I know this probably isn’t the right place to ask this, but I can’t get an answer at stackOverflow and Why3 doesn’t really have a community or an easy way to ask questions…
So I have this definition in Coq:
Fixpoint executeBool (state:M.t Z) (stack:list Z) (program:list insStBool) : list Z := match program with [...] | (SBSkip O)::l => executeBool state stack l | (SBSkip (S n))::l => executeBool_skip n state stack l [...] end with executeBool_skip n (state:M.t Z) (stack:list Z) (program:list insStBool) : list Z := match program with [...] end.
And I’m trying to translate that code to Why3 and everything works except for
executeBool_skip because that “with” notation, apparently, doesn’t exist… Is there a way to define
executeBool_skip using a similar “with” notation (that is
with executeBool_skip n…) but in Why3? I can’t define
executeBool_skip before or after because it uses
executeBool (and vice-versa).
Thank you and sorry for not being in the right topic.