(*******************************************************************************)
(* Coq Unit Testing project                                                    *)
(* Copyright 2018 Catherine Dubois and Alain Giorgetti                         *)
(* Samovar - FEMTO-ST institute                                                *)
(*******************************************************************************)

(*******************************************************************************)
(*      This file is distributed under the terms of the                        *)
(*       GNU Lesser General Public License Version 2.1                         *)
(*******************************************************************************)

(** [it_interval n] is a bounded exhaustive generator of elements in 
    the initial interval of natural numbers [[0..n-1]]. *)

Require Import List Nat.

Require Import mathcomp.ssreflect.ssreflect.
From QuickChick Require Import QuickChick.

(* begin hide *)
Set Warnings "-extraction-opaque-accessed,-extraction".
(* end hide *)

Require Import Sc.

Definition it_interval (n : nat) := {|
 st_t    := nat * nat;
 start   := (0, n);
 next    := fun st => 
              match st with
               (cur, upper) => (Some (S cur), (S cur, upper))
              end;
 hasnext := fun st =>
              match st with 
               (cur, upper) => ltb cur upper
              end
|}.