(*******************************************************************************)
(* Coq Unit Testing project                                                    *)
(* Copyright 2018-2020 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_endofun n] is a bounded exhaustive generator for endofunctions in [[0..n-1]].
    Endofunctions are defined in [endofun.v]. *)

Require Import Arith List NPeano String Nat.

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

Require Import cut Sc sc_endoline.

Definition it_endofun (n : nat) := {|
 st_t    := st_t (it_endo n);
 start   := start (it_endo n);
 next    := fun c =>
             let (f,c') := (next (it_endo n)) c in
             match f with
               None   => (None, c')
             | Some l => (Some (list2fun l), c')
             end;
 hasnext := hasnext (it_endo n)
|}.


