Nuprl Definition : cmp-type
cmp-type(T;cmp) == x,y:T//((cmp x y) = 0 ∈ ℤ)
Definitions occuring in Statement :
quotient: x,y:A//B[x; y],
apply: f a,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
quotient: x,y:A//B[x; y],
equal: s = t ∈ T,
int: ℤ,
apply: f a,
natural_number: $n
FDL editor aliases :
cmp-type
Latex:
cmp-type(T;cmp) == x,y:T//((cmp x y) = 0)
Date html generated:
2016_05_14-PM-02_37_24
Last ObjectModification:
2015_09_22-PM-05_56_50
Theory : list_1
Home
Index