diff options
Diffstat (limited to 'test-suite/success/coercions.v')
-rw-r--r-- | test-suite/success/coercions.v | 29 |
1 files changed, 25 insertions, 4 deletions
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. +*) + |