Nuprl Definition : eq_id

a = b ==  IdDeq a b


Definitions occuring in Statement :  id-deq: IdDeq,  apply: f a
Definitions occuring in definition :  apply: f a,  id-deq: IdDeq
FDL editor aliases :  eq_id
Latex:
a  =  b  ==    IdDeq  a  b


Date html generated: 2016_05_14-PM-03_37_11
Last ObjectModification: 2015_09_22-PM-06_01_37

Theory : decidable!equality


Home Index