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

(*
fn main() {
    fn foo() -> ! {
        panic!("This call never returns.");
    }
}
*)
Definition main (ε : 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_main : M.IsFunction "diverging_functions::main" main.

Module main.
  (*
      fn foo() -> ! {
          panic!("This call never returns.");
      }
  *)
  Definition foo (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (M.call_closure (|
          M.get_function (|
            "std::panicking::begin_panic",
            [ Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ]
          |),
          [ M.read (| Value.String "This call never returns." |) ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_foo : M.IsFunction "diverging_functions::main::foo" foo.
End main.
