Nuprl Definition : nat-missing-type
nat-missing-type() == m:{m:ℤ| (-1) ≤ m} × {L:ℕ List| l-ordered(ℕ;x,y.x < y;L) ∧ (∀x∈L.x < m)}
Definitions occuring in Statement :
l_all: (∀x∈L.P[x]),
list: T List,
nat: ℕ,
less_than: a < b,
le: A ≤ B,
and: P ∧ Q,
set: {x:A| B[x]} ,
product: x:A × B[x],
minus: -n,
natural_number: $n,
int: ℤ
FDL editor aliases :
nat-missing-type
Latex:
nat-missing-type() == m:\{m:\mBbbZ{}| (-1) \mleq{} m\} \mtimes{} \{L:\mBbbN{} List| l-ordered(\mBbbN{};x,y.x < y;L) \mwedge{} (\mforall{}x\mmember{}L.x < m)\}
Date html generated:
2016_05_17-PM-01_44_50
Last ObjectModification:
2013_04_01-PM-00_50_35
Theory : datatype-signatures
Home
Index