fact: Fixpoint execute (stack : list nat) (prog : list sinstr) : list nat := match (prog, stack) with | (nil, _ ) => stack | (SPush n::prog', _ ) => execute (n::stack) prog' | (SPlus::prog', m::n::stack') => execute ((m+n)::stack') prog' | (SMinus::prog', m::n::stack') => execute ((m-n)::stack') prog' | (SMult::prog', m::n::stack') => execute ((m*n)::stack') prog' | (_::prog', _ ) => execute stack prog' end.
imports: QuickChick(QuickChick) Arith List Stack.Exp