Nuprl Definition : eo_record
eo_record{i:l}() ==
"E":Type
"dom":self."E" ─→ 𝔹
"<":self."E" ⟶ self."E" ─→ ℙ
"locless":self."E" ─→ self."E" ─→ 𝔹
"loc":self."E" ─→ Id
"pred":self."E" ─→ self."E"
"rank":self."E" ─→ ℕ
Definitions occuring in Statement :
Id: Id,
nat: ℕ,
bool: 𝔹,
top: Top,
prop: ℙ,
function: x:A ─→ B[x],
token: "$token",
universe: Type,
record-select: r.x,
record+: record+,
record: record(x.T[x])
FDL editor aliases :
eo_record
eo\_record\{i:l\}() ==
"E":Type
"dom":self."E" {}\mrightarrow{} \mBbbB{}
"<":self."E" {}\mrightarrow{} self."E" {}\mrightarrow{} \mBbbP{}
"locless":self."E" {}\mrightarrow{} self."E" {}\mrightarrow{} \mBbbB{}
"loc":self."E" {}\mrightarrow{} Id
"pred":self."E" {}\mrightarrow{} self."E"
"rank":self."E" {}\mrightarrow{} \mBbbN{}
Date html generated:
2015_07_17-AM-08_33_41
Last ObjectModification:
2014_02_20-PM-09_20_09
Home
Index