Coq to Why3: with notation

Miscellaneous
1

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.

2

I think the syntax is

function foo ... = ...
with bar ... = ...
1 Like