EventsWithOrder ==
E:Type
eq:EqDecider(E)
pred?:E 
(?E)
info:E (Id Top + (IdLnk E Top))
oaxioms:EOrderAxioms(E;pred?;info)
Top
Definitions :
universe: Type,
deq: EqDecider(T),
unit: Unit,
function: x:A B[x],
union: left + right,
Id: Id,
IdLnk: IdLnk,
product: x:A B[x],
top: Top
FDL editor aliases :
EOrder
EventsWithOrder ==
E:Type
\mtimes{} eq:EqDecider(E)
\mtimes{} pred?:E {}\mrightarrow{} (?E)
\mtimes{} info:E {}\mrightarrow{} (Id \mtimes{} Top + (IdLnk \mtimes{} E \mtimes{} Top))
\mtimes{} oaxioms:EOrderAxioms(E;pred?;info)
\mtimes{} Top
Date html generated:
2010_08_27-AM-01_08_00
Last ObjectModification:
2009_12_16-AM-12_35_56
Home
Index