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

Module checked.
  (*
  Enum MathError
  {
    const_params := [];
    ty_params := [];
    variants :=
      [
        {
          name := "DivisionByZero";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "NonPositiveLogarithm";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "NegativeSquareRoot";
          item := StructTuple [];
          discriminant := None;
        }
      ];
  }
  *)
  
  Module Impl_core_fmt_Debug_for_result_chaining_with_question_mark_checked_MathError.
    Definition Self : Ty.t := Ty.path "result_chaining_with_question_mark::checked::MathError".
    
    Parameter fmt : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Debug"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Debug_for_result_chaining_with_question_mark_checked_MathError.
  
  Axiom MathResult :
    (Ty.path "result_chaining_with_question_mark::checked::MathResult") =
      (Ty.apply
        (Ty.path "core::result::Result")
        []
        [ Ty.path "f64"; Ty.path "result_chaining_with_question_mark::checked::MathError" ]).
  
  Parameter div : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_div : M.IsFunction "result_chaining_with_question_mark::checked::div" div.
  
  Parameter sqrt : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_sqrt : M.IsFunction "result_chaining_with_question_mark::checked::sqrt" sqrt.
  
  Parameter ln : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_ln : M.IsFunction "result_chaining_with_question_mark::checked::ln" ln.
  
  Parameter op_ : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_op_ : M.IsFunction "result_chaining_with_question_mark::checked::op_" op_.
  
  Parameter op : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_op : M.IsFunction "result_chaining_with_question_mark::checked::op" op.
End checked.

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

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