Nuprl Definition : deq-witness
deq-witness(eq) == λx,y. if eq x y then inl Ax else inr (λz.Ax) fi
Definitions occuring in Statement :
ifthenelse: if b then t else f fi ,
apply: f a,
lambda: λx.A[x],
inr: inr x ,
inl: inl x,
axiom: Ax
Definitions occuring in definition :
ifthenelse: if b then t else f fi ,
apply: f a,
inl: inl x,
inr: inr x ,
lambda: λx.A[x],
axiom: Ax
FDL editor aliases :
deq-witness
Latex:
deq-witness(eq) == \mlambda{}x,y. if eq x y then inl Ax else inr (\mlambda{}z.Ax) fi
Date html generated:
2016_05_14-AM-06_06_38
Last ObjectModification:
2015_09_22-PM-05_48_11
Theory : equality!deciders
Home
Index