(* 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_Marker.
Export Core_Marker.

Record t_Range (v_Idx : Type) `{t_Sized (v_Idx)} : Type :=
  {
    Range_f_start : v_Idx;
    Range_f_end : v_Idx;
  }.
Arguments Build_t_Range (_) {_}.
Arguments Range_f_start {_} {_}.
Arguments Range_f_end {_} {_}.
#[export] Instance settable_t_Range `{v_Idx : Type} `{t_Sized (v_Idx)} : Settable _ :=
  settable! (Build_t_Range v_Idx) <Range_f_start; Range_f_end>.
