WhoCites
Definitions
mb
structures
Sections
GenAutomata
Doc
Who Cites msg
content?
msg_content
Def content(MS) == 1of(2of(2of(MS)))
Thm*
M:MessageStruct. content(M)
|M|
|cEQ(M)|
pi2
Def
2of(t) == t.2
Thm*
A:Type, B:(A
Type), p:(a:A
B(a)). 2of(p)
B(1of(p))
pi1
Def
1of(t) == t.1
Thm*
A:Type, B:(A
Type), p:(a:A
B(a)). 1of(p)
A
Syntax:
content(MS)
has structure:
msg_content(MS)
About:
WhoCites
Definitions
mb
structures
Sections
GenAutomata
Doc