(* File automatically generated by Hacspec *)
From Coq Require Import ZArith.
Require Import List.
Import List.ListNotations.
Open Scope Z_scope.
Open Scope bool_scope.
Require Import Ascii.
Require Import String.
Require Import Coq.Floats.Floats.
From RecordUpdate Require Import RecordSet.
Import RecordSetNotations.

(* From Core Require Import Core. *)

From Core Require Import Core_Clone.
Export Core_Clone.

From Core Require Import Core_Marker (t_Sized).
Export Core_Marker (t_Sized).

From Core Require Import Core_Panicking (panic).
Export Core_Panicking (panic).

From Core Require Import Core_Ops_Function.
Export Core_Ops_Function.

Inductive t_Option (v_T : Type) `{t_Sized (v_T)} : Type :=
| Option_None
| Option_Some : v_T -> _.
Arguments Option_None {_} {_}.
Arguments Option_Some {_} {_}.

Instance t_Clone_390068633 `{v_T : Type} `{t_Sized (v_T)} `{t_Clone (v_T)} : t_Clone ((t_Option ((v_T)))) :=
  {
    Clone_f_clone := fun  (self : t_Option ((v_T)))=>
      match self with
      | Option_Some (x) =>
        Option_Some (Clone_f_clone (x))
      | Option_None =>
        Option_None
      end;
  }.

Definition impl_1__is_some `{v_T : Type} `{t_Sized (v_T)} (self : t_Option ((v_T))) : bool :=
  match self with
  | Option_Some (_) =>
    true
  | _ =>
    false
  end.

Program Definition impl__map `{v_T : Type} `{v_U : Type} `{v_F : Type} `{t_Sized (v_T)} `{t_Sized (v_U)} `{t_Sized (v_F)} `{t_FnOnce (v_F) ((v_T))} `{_.(FnOnce_f_Output) = v_U} (self : t_Option ((v_T))) (f : v_F) : t_Option ((v_U)) :=
  match self with
  | Option_Some (x) =>
    Option_Some _ (* (FnOnce_f_call_once (f) ((x))) *)
  | Option_None =>
    Option_None
  end.
Next Obligation.
  refine (FnOnce_f_call_once (f) ((x))).
Defined.
Fail Next Obligation.

(* Definition unwrap_failed '(_ : unit) : t_Never := *)
(*   panic ("called `Option::unwrap()` on a `None` value"%string). *)

(* Definition impl_1__unwrap `{v_T : Type} `{t_Sized (v_T)} (self : t_Option ((v_T))) `{impl_1__is_some (self___) = true} : v_T := *)
(*   match self with *)
(*   | Option_Some (val) => *)
(*     val *)
(*   | Option_None => *)
(*     never_to_any (unwrap_failed (tt)) *)
(*   end. *)

(* Definition expect_failed (msg : string) : t_Never := *)
(*   panic (msg). *)

(* Definition impl_1__expect `{v_T : Type} `{t_Sized (v_T)} (self : t_Option ((v_T))) (msg : string) : v_T := *)
(*   match self with *)
(*   | Option_Some (val) => *)
(*     val *)
(*   | Option_None => *)
(*     never_to_any (expect_failed (msg)) *)
(*   end. *)
