Nuprl Definition : message-cmp
message-cmp(hdrs;mcmp) ==
comparison-seq(compare-fun(bool-cmp();λm.msg-authentic(m));
comparison-seq(list-index-cmp(NameDeq;hdrs;λm.msg-header(m)); msg-body-cmp(mcmp)))
Definitions occuring in Statement :
msg-body-cmp: msg-body-cmp(mcmp),
msg-header: msg-header(m),
msg-authentic: msg-authentic(m),
name-deq: NameDeq,
list-index-cmp: list-index-cmp(eq;L;f),
comparison-seq: comparison-seq(c1; c2),
compare-fun: compare-fun(cmp;f),
bool-cmp: bool-cmp(),
lambda: λx.A[x]
FDL editor aliases :
message-cmp
Latex:
message-cmp(hdrs;mcmp) ==
comparison-seq(compare-fun(bool-cmp();\mlambda{}m.msg-authentic(m));
comparison-seq(list-index-cmp(NameDeq;hdrs;\mlambda{}m.msg-header(m)); msg-body-cmp(mcmp)))
Date html generated:
2016_05_17-AM-09_03_26
Last ObjectModification:
2014_07_25-PM-05_04_13
Theory : messages
Home
Index