blob: 750165a55ad886a88fb4157d4a377d4eb5a59f3e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
|
(* Interaction between coercions and casts *)
(* Example provided by Eduardo Gimenez *)
Parameter Z S : Set.
Parameter f : S -> Z.
Coercion f : S >-> Z.
Parameter g : Z -> Z.
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 decided 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.
*)
(* Check coercion between products based on eta-expansion *)
(* (there was a de Bruijn bug until rev ) *)
Section P.
Variable E : Set.
Variables C D : E -> Prop.
Variable G :> forall x, C x -> D x.
Check fun (H : forall y:E, y = y -> C y) => (H : forall y:E, y = y -> D y).
End P.
|
