diff options
author | Stephane Glondu <steph@glondu.net> | 2008-09-08 00:15:04 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2008-09-08 00:15:04 +0200 |
commit | 113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (patch) | |
tree | c260a140410c796f113584a2f7e6b9b7f6e00aa5 /test-suite/success/coercions.v | |
parent | 870075f34dd9fa5792bfbf413afd3b96f17e76a0 (diff) |
Imported Upstream version 8.2~beta4.svn20080907+dfsgupstream/8.2.beta4.svn20080907+dfsg
Diffstat (limited to 'test-suite/success/coercions.v')
-rw-r--r-- | test-suite/success/coercions.v | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v index d652132e..525348de 100644 --- a/test-suite/success/coercions.v +++ b/test-suite/success/coercions.v @@ -61,3 +61,24 @@ Check fun (H : For_all (fun x => C (f x))) => H : For_all (fun x => D (f x)). End Q. +(* Combining class lookup and path lookup so that if a lookup fails, another + descent in the class can be found (see wish #1934) *) + +Record Setoid : Type := +{ car :> Type }. + +Record Morphism (X Y:Setoid) : Type := +{evalMorphism :> X -> Y}. + +Definition extSetoid (X Y:Setoid) : Setoid. +intros X Y. +constructor. +exact (Morphism X Y). +Defined. + +Definition ClaimA := forall (X Y:Setoid) (f: extSetoid X Y) x, f x= f x. + +Coercion irrelevent := (fun _ => I) : True -> car (Build_Setoid True). + +Definition ClaimB := forall (X Y:Setoid) (f: extSetoid X Y) (x:X), f x= f x. + |