diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:28 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:28 -0500 |
commit | 1ef7f1c0c6897535a86daa77799714e25638f5e9 (patch) | |
tree | 5bcca733632ecc84d2c6b1ee48cb2e557a7adba5 /test-suite/misc/7595/base.v | |
parent | 3a2fac7bcee36fd9dcb4f39a615c8ac0349abcc9 (diff) | |
parent | 9ebf44d84754adc5b64fcf612c6816c02c80462d (diff) |
Updated version 8.9.0 from 'upstream/8.9.0'
with Debian dir 81a4f85bc45e59aa1eadb4797f0eb0b8039efb63
Diffstat (limited to 'test-suite/misc/7595/base.v')
-rw-r--r-- | test-suite/misc/7595/base.v | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/test-suite/misc/7595/base.v b/test-suite/misc/7595/base.v new file mode 100644 index 00000000..6a6b7b79 --- /dev/null +++ b/test-suite/misc/7595/base.v @@ -0,0 +1,28 @@ +From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid. +Set Default Proof Using "Type". +Export ListNotations. +From Coq.Program Require Export Basics Syntax. +Global Generalizable All Variables. + +(** * Type classes *) +(** ** Decidable propositions *) +(** This type class by (Spitters/van der Weegen, 2011) collects decidable +propositions. *) +Class Decision (P : Prop) := decide : {P} + {¬P}. +Hint Mode Decision ! : typeclass_instances. +Arguments decide _ {_} : simpl never, assert. + +(** ** Proof irrelevant types *) +(** This type class collects types that are proof irrelevant. That means, all +elements of the type are equal. We use this notion only used for propositions, +but by universe polymorphism we can generalize it. *) +Class ProofIrrel (A : Type) : Prop := proof_irrel (x y : A) : x = y. +Hint Mode ProofIrrel ! : typeclass_instances. + +Class MGuard (M : Type → Type) := + mguard: ∀ P {dec : Decision P} {A}, (P → M A) → M A. +Arguments mguard _ _ _ !_ _ _ / : assert. +Notation "'guard' P ; z" := (mguard P (λ _, z)) + (at level 20, z at level 200, only parsing, right associativity) . +Notation "'guard' P 'as' H ; z" := (mguard P (λ H, z)) + (at level 20, z at level 200, only parsing, right associativity) . |