Nuprl Definition : ctt-opr-is
ctt-opr-is(f;s) == let k,v = f in k =a "opid" ∧b v =a s
Definitions occuring in Statement :
band: p ∧b q,
eq_atom: x =a y,
spread: spread def,
token: "$token"
Definitions occuring in definition :
spread: spread def,
band: p ∧b q,
token: "$token",
eq_atom: x =a y
FDL editor aliases :
ctt-opr-is
Latex:
ctt-opr-is(f;s) == let k,v = f in k =a "opid" \mwedge{}\msubb{} v =a s
Date html generated:
2020_05_20-PM-08_20_50
Last ObjectModification:
2020_02_15-AM-10_57_09
Theory : cubical!type!theory
Home
Index