-
Coercion between inductive types
Coq < Definition bool_in_nat := [b:bool]if b then O else (S O).
bool_in_nat is defined
Coq < Coercion bool_in_nat : bool >-> nat.
bool_in_nat is now a coercion
Coq < Check O=true.
O=(true)
: Prop
Warning:
Check true=O. fails. This is ``normal'' behaviour of
coercions. To validate true=O, the coercion is searched from
nat to bool. There is no one.
- Coercion to a sort
Coq < Variable Graph : Type.
Graph is assumed
Coq < Variable Node : Graph -> Type.
Node is assumed
Coq < Coercion Node : Graph >-> SORTCLASS.
Node is now a coercion
Coq < Variable G : Graph.
G is assumed
Coq < Variable Arrows : G -> G -> Type.
Arrows is assumed
Coq < Check Arrows.
Arrows
: (G)->(G)->Type
Coq < Variable fg : G -> G.
fg is assumed
Coq < Check fg.
fg
: (G)->(G)
- Coercion to a function
Coq < Variable bij : Set -> Set -> Set.
bij is assumed
Coq < Variable ap : (A,B:Set)(bij A B) -> A -> B.
ap is assumed
Coq < Coercion ap : bij >-> FUNCLASS.
ap is now a coercion
Coq < Variable b : (bij nat nat).
b is assumed
Coq < Check (b O).
(ap nat nat b O)
: nat
- Transitivity of coercion
Coq < Variables C : nat -> Set; D : nat -> bool -> Set; E : bool -> Set.
C is assumed
D is assumed
E is assumed
Coq < Variable f : (n:nat)(C n) -> (D (S n) true).
f is assumed
Coq < Coercion f : C >-> D.
f is now a coercion
Coq < Variable g : (n:nat)(b:bool)(D n b) -> (E b).
g is assumed
Coq < Coercion g : D >-> E.
g is now a coercion
Coq < Variable c : (C O).
c is assumed
Coq < Variable T : (E true) -> nat.
T is assumed
Coq < Check (T c).
(T (c))
: nat
- Identity coercion
Coq < Definition D' := [b:bool](D (S O) b).
D' is defined
Coq < Identity Coercion IdD'D : D' >-> D.
IdD'D is now a coercion
Coq < Print IdD'D.
IdD'D = [b:bool; x:(D' b)]x
: (b:bool)(D' b)->(D (S O) b)
Coq < Variable d' : (D' true).
d' is assumed
Coq < Check (T d').
(T (d'))
: nat
