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

(** Bounded exhaustive tests with the generator defined in [sc_interval.v]. *)

Require Import Arith NPeano Nat.

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

Require Import Sc sc_interval.

(** *** Each enumerated number (of the interval $[0..7]$) is less than or equal to 7? *)

SmallCheck (it_interval 7) (fun x : nat => leb x 7).

(** Output: Success *)

(** *** Each enumerated number is less than or equal to 6? *)

SmallCheck (it_interval 7) (fun x : nat => leb x 6).

(** Output: Failure: 7 *)
