Nuprl Definition : in-context-dom
in-context-dom(ctxt;v) == let X,vs,f = ctxt in (v ∈ vs)
Definitions occuring in Statement :
varname: varname(),
l_member: (x ∈ l),
spreadn: spread3
Definitions occuring in definition :
spreadn: spread3,
l_member: (x ∈ l),
varname: varname()
FDL editor aliases :
in-context-dom
Latex:
in-context-dom(ctxt;v) == let X,vs,f = ctxt in (v \mmember{} vs)
Date html generated:
2020_05_20-PM-08_02_01
Last ObjectModification:
2020_02_25-PM-03_39_43
Theory : cubical!type!theory
Home
Index