Nuprl Definition : ctt-op
CttOp ==
k:{k:Atom| (k ∈ ``opid nType nterm univ``)} × if k =a "opid" then {f:Atom| (f ∈ ctt-tokens())}
if k =a "nType" then Type
if k =a "nterm" then T:Type × T
else ℕ
fi
Definitions occuring in Statement :
ctt-tokens: ctt-tokens(),
l_member: (x ∈ l),
cons: [a / b],
nil: [],
nat: ℕ,
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
set: {x:A| B[x]} ,
product: x:A × B[x],
token: "$token",
atom: Atom,
universe: Type
Definitions occuring in definition :
cons: [a / b],
nil: [],
set: {x:A| B[x]} ,
l_member: (x ∈ l),
ctt-tokens: ctt-tokens(),
atom: Atom,
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
token: "$token",
product: x:A × B[x],
universe: Type,
nat: ℕ
FDL editor aliases :
ctt-op
Latex:
CttOp ==
k:\{k:Atom| (k \mmember{} ``opid nType nterm univ``)\} \mtimes{} if k =a "opid" then \{f:Atom| (f \mmember{} ctt-tokens())\}
if k =a "nType" then Type
if k =a "nterm" then T:Type \mtimes{} T
else \mBbbN{}
fi
Date html generated:
2020_05_20-PM-08_16_24
Last ObjectModification:
2020_02_10-PM-01_07_11
Theory : cubical!type!theory
Home
Index