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

Parameter eat_box_i32 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.

Axiom Function_eat_box_i32 : M.IsFunction "scoping_rules_borrowing::eat_box_i32" eat_box_i32.

Parameter borrow_i32 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.

Axiom Function_borrow_i32 : M.IsFunction "scoping_rules_borrowing::borrow_i32" borrow_i32.

Parameter main : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.

Axiom Function_main : M.IsFunction "scoping_rules_borrowing::main" main.
