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

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

Axiom Function_function : M.IsFunction "the_use_as_declaration::function" function.

Module deeply.
  Module nested.
    Parameter function : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_function :
      M.IsFunction "the_use_as_declaration::deeply::nested::function" function.
  End nested.
End deeply.

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

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