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
Latex:
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:
2016_05_16-AM-09_13_18
Last ObjectModification:
2014_02_21-PM-02_29_33
Theory : new!event-ordering
Home
Index