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

(*
fn some_fn() {
    ()
}
*)
Definition some_fn (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [] => ltac:(M.monadic (Value.Tuple []))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_some_fn : M.IsFunction "diverging_functions_no_info_in_return_type::some_fn" some_fn.

(*
fn main() {
    let a: () = some_fn();
    println!("This function returns and you can see this line.")
}
*)
Definition main (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [] =>
    ltac:(M.monadic
      (M.read (|
        let~ a :=
          M.alloc (|
            M.call_closure (|
              M.get_function (| "diverging_functions_no_info_in_return_type::some_fn", [] |),
              []
            |)
          |) in
        let~ _ :=
          M.alloc (|
            M.call_closure (|
              M.get_function (| "std::io::stdio::_print", [] |),
              [
                M.call_closure (|
                  M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_const", [] |),
                  [
                    M.alloc (|
                      Value.Array
                        [
                          M.read (|
                            Value.String "This function returns and you can see this line.
"
                          |)
                        ]
                    |)
                  ]
                |)
              ]
            |)
          |) in
        M.alloc (| Value.Tuple [] |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

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