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