(* 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. *)

Inductive t_Never : Type :=
.

Definition t_Never_cast_to_repr (x : t_Never) : t_Never :=
  match x with
  end.

Definition never_to_any `{v_T : Type} (x : t_Never) : v_T :=
  (match x with
  end).

Definition panic (expr : string) {HFalse : t_Never} : t_Never :=
  never_to_any HFalse.

Definition panic_explicit '(_ : unit) `{HFalse : t_Never} : t_Never :=
  never_to_any HFalse.
