(*******************************************************************************)
(* 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_permut n] is a bounded exhaustive generator for permutations on
 [[0..n-1]], as defined in [permut.v]. It is based on [it_permline] and [list2fun]. *)

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

Require Import cut Sc sc_permline.

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