Expand description
Congruence lemmas for parser, serializer, and preparation specifications.
Functionsยง
- lemma_
alt_ parser_ congruence - lemma_
alt_ prepare_ congruence - lemma_
alt_ serializer_ congruence - lemma_
alt_ spec_ parse_ congruence - lemma_
and_ then_ parser_ congruence - lemma_
and_ then_ prepare_ congruence - lemma_
and_ then_ serializer_ congruence - lemma_
and_ then_ spec_ parse_ congruence - lemma_
array_ parser_ congruence - lemma_
array_ prepare_ congruence - lemma_
array_ serializer_ congruence - lemma_
bind_ parser_ congruence - lemma_
bind_ prepare_ congruence - lemma_
bind_ serializer_ congruence - lemma_
bind_ spec_ parse_ congruence - lemma_
bits_ parser_ congruence - lemma_
bits_ prepare_ congruence - lemma_
bits_ serializer_ congruence - lemma_
choice_ parser_ congruence - lemma_
choice_ prepare_ congruence - lemma_
choice_ serializer_ congruence - lemma_
choice_ spec_ parse_ congruence - lemma_
cond_ parser_ congruence - lemma_
cond_ prepare_ congruence - lemma_
cond_ serializer_ congruence - lemma_
cond_ spec_ parse_ congruence - lemma_
const_ parser_ congruence - lemma_
const_ prepare_ congruence - lemma_
const_ serializer_ congruence - lemma_
const_ spec_ parse_ congruence - lemma_
exact_ len_ parser_ congruence - lemma_
exact_ len_ prepare_ congruence - lemma_
exact_ len_ serializer_ congruence - lemma_
exact_ len_ spec_ parse_ congruence - lemma_
mapped_ parser_ congruence - lemma_
mapped_ prepare_ congruence - lemma_
mapped_ serializer_ congruence - lemma_
mapped_ spec_ parse_ congruence - lemma_
named_ parser_ congruence - lemma_
named_ prepare_ congruence - lemma_
named_ serializer_ congruence - lemma_
named_ spec_ parse_ congruence - lemma_
opt_ parser_ congruence - lemma_
opt_ prepare_ congruence - lemma_
opt_ serializer_ congruence - lemma_
opt_ spec_ parse_ congruence - lemma_
optional_ end_ parser_ congruence - lemma_
optional_ end_ prepare_ congruence - lemma_
optional_ end_ serializer_ congruence - lemma_
optional_ end_ spec_ parse_ congruence - lemma_
optional_ parser_ congruence - lemma_
optional_ prepare_ congruence - lemma_
optional_ serializer_ congruence - lemma_
optional_ spec_ parse_ congruence - lemma_
pair_ parser_ congruence - lemma_
pair_ prepare_ congruence - lemma_
pair_ serializer_ congruence - lemma_
pair_ spec_ parse_ congruence - lemma_
parser_ congruent_ apply - lemma_
parser_ congruent_ intro - lemma_
parser_ congruent_ reflexive - lemma_
parser_ congruent_ symmetric - lemma_
parser_ congruent_ transitive - lemma_
preceded_ parser_ congruence - lemma_
preceded_ prepare_ congruence - lemma_
preceded_ serializer_ congruence - lemma_
preceded_ spec_ parse_ congruence - lemma_
prefix_ tagged_ parser_ congruence - lemma_
prefix_ tagged_ prepare_ congruence - lemma_
prefix_ tagged_ serializer_ congruence - lemma_
prepare_ congruent_ byte_ len - lemma_
prepare_ congruent_ consistent - lemma_
prepare_ congruent_ intro - lemma_
prepare_ congruent_ reflexive - lemma_
prepare_ congruent_ symmetric - lemma_
prepare_ congruent_ transitive - lemma_
ref_ fn_ parser_ congruence - lemma_
ref_ parser_ congruence - lemma_
ref_ prepare_ congruence - lemma_
ref_ serializer_ congruence - lemma_
ref_ spec_ parse_ congruence - lemma_
refined_ parser_ congruence - lemma_
refined_ prepare_ congruence - lemma_
refined_ serializer_ congruence - lemma_
refined_ spec_ parse_ congruence - lemma_
repeat_ n_ parse_ n_ rec_ congruence - lemma_
repeat_ n_ parser_ congruence - lemma_
repeat_ n_ prepare_ congruence - lemma_
repeat_ n_ serializer_ congruence - lemma_
repeat_ n_ spec_ parse_ congruence - lemma_
repeat_ parser_ congruence - lemma_
repeat_ prepare_ congruence - lemma_
repeat_ serializer_ congruence - lemma_
repeat_ spec_ parse_ congruence - lemma_
repeat_ till_ end_ parser_ congruence - lemma_
repeat_ till_ end_ prepare_ congruence - lemma_
repeat_ till_ end_ serializer_ congruence - lemma_
repeat_ till_ end_ spec_ parse_ congruence - lemma_
serializer_ congruent_ intro - lemma_
serializer_ congruent_ prepare - lemma_
serializer_ congruent_ reflexive - lemma_
serializer_ congruent_ serialize - lemma_
serializer_ congruent_ symmetric - lemma_
serializer_ congruent_ transitive - lemma_
star_ parse_ rec_ congruence - lemma_
star_ parser_ congruence - lemma_
star_ prepare_ congruence - lemma_
star_ serializer_ congruence - lemma_
star_ spec_ parse_ congruence - lemma_
suffix_ tagged_ parser_ congruence - lemma_
suffix_ tagged_ prepare_ congruence - lemma_
suffix_ tagged_ serializer_ congruence - lemma_
sum_ parser_ congruence - lemma_
sum_ prepare_ congruence - lemma_
sum_ serializer_ congruence - lemma_
sum_ spec_ parse_ congruence - lemma_
terminated_ parser_ congruence - lemma_
terminated_ prepare_ congruence - lemma_
terminated_ serializer_ congruence - lemma_
terminated_ spec_ parse_ congruence - parser_
congruence_ lemmas - parser_
congruent - prepare_
congruence_ lemmas - prepare_
congruent - serializer_
congruence_ lemmas - serializer_
congruent