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

Module my_mod.
  Parameter private_function : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_private_function :
    M.IsFunction "visibility::my_mod::private_function" private_function.
  
  Parameter function : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_function : M.IsFunction "visibility::my_mod::function" function.
  
  Parameter indirect_access : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_indirect_access :
    M.IsFunction "visibility::my_mod::indirect_access" indirect_access.
  
  Module nested.
    Parameter function : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_function : M.IsFunction "visibility::my_mod::nested::function" function.
    
    Parameter private_function : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_private_function :
      M.IsFunction "visibility::my_mod::nested::private_function" private_function.
    
    Parameter public_function_in_my_mod : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_public_function_in_my_mod :
      M.IsFunction
        "visibility::my_mod::nested::public_function_in_my_mod"
        public_function_in_my_mod.
    
    Parameter public_function_in_nested : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_public_function_in_nested :
      M.IsFunction
        "visibility::my_mod::nested::public_function_in_nested"
        public_function_in_nested.
    
    Parameter public_function_in_super_mod : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_public_function_in_super_mod :
      M.IsFunction
        "visibility::my_mod::nested::public_function_in_super_mod"
        public_function_in_super_mod.
  End nested.
  
  Parameter call_public_function_in_my_mod : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_call_public_function_in_my_mod :
    M.IsFunction
      "visibility::my_mod::call_public_function_in_my_mod"
      call_public_function_in_my_mod.
  
  Parameter public_function_in_crate : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_public_function_in_crate :
    M.IsFunction "visibility::my_mod::public_function_in_crate" public_function_in_crate.
  
  Module private_nested.
    Parameter function : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_function : M.IsFunction "visibility::my_mod::private_nested::function" function.
    
    Parameter restricted_function : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_restricted_function :
      M.IsFunction "visibility::my_mod::private_nested::restricted_function" restricted_function.
  End private_nested.
End my_mod.

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

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

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

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