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
Latex:
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:
2016_05_16-AM-09_13_14
Last ObjectModification:
2014_02_20-PM-09_20_09
Theory : new!event-ordering
Home
Index