Add Normalform and ShareableArgs instances for Property #211

FreeProving · Sep 30, 2020 · 2020e68 · 2020e68
1 parent e2c951b
commit 2020e68
Showing 1 changed file with 12 additions and 0 deletions.
diff --git a/base/coq/Test/QuickCheck.v b/base/coq/Test/QuickCheck.v
@@ -4,6 +4,18 @@ From Base Require Import Prelude.
 (* QuickCheck properties are implemented as Coq propositions. *)
 Definition Property (Shape : Type) (Pos : Shape -> Type) := Prop.
 
+(* Normalform instance for Property. *)
+Instance NormalformProperty (Shape : Type) (Pos : Shape -> Type)
+  : Normalform Shape Pos (Property Shape Pos) := {
+    nf' := pure
+}.
+
+(* ShareableArgs instance for Property. *)
+Instance ShareableArgsProperty (Shape : Type) (Pos : Shape -> Type)
+  : ShareableArgs Shape Pos (Property Shape Pos) := {
+    shareArgs := pure
+}.
+
 (* * [Testable] type class *)
 
 (* [class Testable prop where property :: prop -> Property] *)