From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- test-suite/success/coercions.v | 29 +++++++++++++++++++++++++---- 1 file changed, 25 insertions(+), 4 deletions(-) (limited to 'test-suite/success/coercions.v') diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v index 98b613ba..8dd48752 100644 --- a/test-suite/success/coercions.v +++ b/test-suite/success/coercions.v @@ -1,11 +1,32 @@ (* Interaction between coercions and casts *) (* Example provided by Eduardo Gimenez *) -Parameter Z,S:Set. +Parameter Z S : Set. -Parameter f: S -> Z. -Coercion f: S >-> Z. +Parameter f : S -> Z. +Coercion f : S >-> Z. Parameter g : Z -> Z. -Check [s](g (s::S)). +Check (fun s => g (s:S)). + + +(* Check uniform inheritance condition *) + +Parameter h : nat -> nat -> Prop. +Parameter i : forall n m : nat, h n m -> nat. +Coercion i : h >-> nat. + +(* Check coercion to funclass when the source occurs in the target *) + +Parameter C : nat -> nat -> nat. +Coercion C : nat >-> Funclass. + +(* Remark: in the following example, it cannot be decide whether C is + from nat to Funclass or from A to nat. An explicit Coercion command is + expected + +Parameter A : nat -> Prop. +Parameter C:> forall n:nat, A n -> nat. +*) + -- cgit v1.2.3