Nuprl Definition : eo-record-type
eo-record-type{i:l}(r) ==
λx.if x =a "E" then Type
if x =a "dom" then r."E" ─→ 𝔹
if x =a "<" then r."E" ─→ r."E" ─→ ℙ
if x =a "locless" then r."E" ─→ r."E" ─→ 𝔹
if x =a "loc" then r."E" ─→ Id
if x =a "pred" then r."E" ─→ r."E"
if x =a "rank" then r."E" ─→ ℕ
else Top
fi
Definitions occuring in Statement :
Id: Id,
nat: ℕ,
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
bool: 𝔹,
top: Top,
prop: ℙ,
lambda: λx.A[x],
function: x:A ─→ B[x],
token: "$token",
universe: Type,
record-select: r.x
FDL editor aliases :
eo-record-type
eo-record-type\{i:l\}(r) ==
\mlambda{}x.if x =a "E" then Type
if x =a "dom" then r."E" {}\mrightarrow{} \mBbbB{}
if x =a "<" then r."E" {}\mrightarrow{} r."E" {}\mrightarrow{} \mBbbP{}
if x =a "locless" then r."E" {}\mrightarrow{} r."E" {}\mrightarrow{} \mBbbB{}
if x =a "loc" then r."E" {}\mrightarrow{} Id
if x =a "pred" then r."E" {}\mrightarrow{} r."E"
if x =a "rank" then r."E" {}\mrightarrow{} \mBbbN{}
else Top
fi
Date html generated:
2015_07_17-AM-08_33_42
Last ObjectModification:
2014_02_21-PM-02_29_33
Home
Index