Nuprl Definition : secret-table
secret-table(T) == K:ℕ × ℕ × (ℕK ─→ (Atom1 × ℕ + Atom1 × data(T)))
Definitions occuring in Statement :
data: data(T),
int_seg: {i..j-},
nat: ℕ,
atom: Atom$n,
function: x:A ─→ B[x],
product: x:A × B[x],
union: left + right,
natural_number: $n
FDL editor aliases :
secret-table
secret-table
secret-table(T) == K:\mBbbN{} \mtimes{} \mBbbN{} \mtimes{} (\mBbbN{}K {}\mrightarrow{} (Atom1 \mtimes{} \mBbbN{} + Atom1 \mtimes{} data(T)))
Date html generated:
2015_07_17-AM-08_55_38
Last ObjectModification:
2013_03_25-PM-01_52_58
Home
Index