(* Generated by coq-of-rust *)
Require Import CoqOfRust.CoqOfRust.

(*
fn add_one(x: u32) -> u32 {
    x + 1
}
*)
Definition add_one (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [ x ] =>
    ltac:(M.monadic
      (let x := M.alloc (| x |) in
      BinOp.Wrap.add (| M.read (| x |), Value.Integer IntegerKind.U32 1 |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_add_one : M.IsFunction "add_one::add_one" add_one.
