Nuprl Definition : coterm-fun
coterm-fun(opr;T) == {v:varname()| ¬(v = nullvar() ∈ varname())} + (opr × ((varname() List × T) List))
Definitions occuring in Statement :
nullvar: nullvar(),
varname: varname(),
list: T List,
not: ¬A,
set: {x:A| B[x]} ,
product: x:A × B[x],
union: left + right,
equal: s = t ∈ T
Definitions occuring in definition :
union: left + right,
set: {x:A| B[x]} ,
not: ¬A,
equal: s = t ∈ T,
nullvar: nullvar(),
product: x:A × B[x],
list: T List
FDL editor aliases :
coterm-fun
Latex:
coterm-fun(opr;T) == \{v:varname()| \mneg{}(v = nullvar())\} + (opr \mtimes{} ((varname() List \mtimes{} T) List))
Date html generated:
2020_05_19-PM-09_53_22
Last ObjectModification:
2020_03_09-PM-04_08_05
Theory : terms
Home
Index