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

(** Handwritten and derived random generators for endofunctions in one-line 
 notation, with QuickChick. See the file [val_qc_endoline.v] for samples and
 tests with these generators. *)

(* begin hide *)
Require Import List Arith Program.
From QuickChick Require Import QuickChick.
Import QcDefaultNotation. Open Scope qc_scope.
Import GenLow GenHigh.
Set Warnings "-extraction-opaque-accessed,-extraction".

Require Import ZArith.
Import ListNotations.

Require Import mathcomp.ssreflect.ssreflect.

Require Import Coq.Strings.String.
Local Open Scope string.

Require Import cut listnat blist endoline qc qc_blist.
(* end hide *)

(** * Handwritten random generator *)

Definition genEndolineAsListnat (n : nat) := genBlistAsListnat n n.

