fact: Fixpoint ceval_fun_no_while (st : state) (c : com) : state := match c with | <{ skip }> => st | <{ x := a }> => (x !-> (aeval st a) ; st) | <{ c1 ; c2 }> => let st' := ceval_fun_no_while st c1 in ceval_fun_no_while st' c2 | <{ if b then c1 else c2 end}> => if (beval st b) then ceval_fun_no_while st c1 else ceval_fun_no_while st c2 | <{ while b do c end }> => st end.
imports: Coq(Bool.Bool) Coq(Init.Nat) Coq(Arith.Arith) Coq(Arith.EqNat) Coq(Lia) Coq(Lists.List) Coq(Strings.String) LF(Maps)