Expand description
Bridges executable invariants through common combinator wrappers.
Functionsยง
- lemma_
alt_ parser_ exec_ inv - lemma_
and_ then_ parser_ exec_ inv - lemma_
and_ then_ prepare_ exec_ inv - lemma_
and_ then_ serializer_ exec_ inv - lemma_
array_ parser_ exec_ inv - lemma_
array_ prepare_ exec_ inv - lemma_
array_ serializer_ exec_ inv - lemma_
bind_ parser_ exec_ inv - lemma_
bind_ prepare_ exec_ inv - lemma_
bind_ serializer_ exec_ inv - lemma_
choice_ parser_ exec_ inv - lemma_
choice_ prepare_ exec_ inv - lemma_
choice_ serializer_ exec_ inv - lemma_
cond_ parser_ exec_ inv - lemma_
cond_ prepare_ exec_ inv - lemma_
cond_ serializer_ exec_ inv - lemma_
const_ parser_ exec_ inv - lemma_
const_ prepare_ exec_ inv - lemma_
const_ serializer_ exec_ inv - lemma_
exact_ len_ parser_ exec_ inv - lemma_
exact_ len_ prepare_ exec_ inv - lemma_
exact_ len_ serializer_ exec_ inv - lemma_
fn_ byte_ len_ specs - lemma_
fn_ prepare_ specs - lemma_
fn_ serializer_ specs - lemma_
mapped_ parser_ exec_ inv - lemma_
mapped_ prepare_ exec_ inv - lemma_
mapped_ serializer_ exec_ inv - lemma_
named_ parser_ exec_ inv - lemma_
named_ prepare_ exec_ inv - lemma_
named_ serializer_ exec_ inv - lemma_
opt_ parser_ exec_ inv - lemma_
opt_ prepare_ exec_ inv - lemma_
opt_ serializer_ exec_ inv - lemma_
optional_ end_ parser_ exec_ inv - lemma_
optional_ end_ prepare_ exec_ inv - lemma_
optional_ end_ serializer_ exec_ inv - lemma_
optional_ parser_ exec_ inv - lemma_
optional_ prepare_ exec_ inv - lemma_
optional_ serializer_ exec_ inv - lemma_
pair_ byte_ len_ exec_ inv - lemma_
pair_ parser_ exec_ inv - lemma_
pair_ prepare_ exec_ inv - lemma_
pair_ serializer_ exec_ inv - lemma_
preceded_ checked_ parser_ exec_ inv - lemma_
preceded_ parser_ exec_ inv - lemma_
preceded_ prepare_ exec_ inv - lemma_
preceded_ serializer_ exec_ inv - lemma_
prefix_ tagged_ parser_ exec_ inv - lemma_
prefix_ tagged_ prepare_ exec_ inv - lemma_
prefix_ tagged_ serializer_ exec_ inv - lemma_
ref_ byte_ len_ exec_ inv - lemma_
ref_ fn_ byte_ len_ congruence - lemma_
ref_ fn_ prepare_ congruence - lemma_
ref_ fn_ serializer_ congruence - lemma_
ref_ parser_ exec_ inv - lemma_
ref_ prepare_ exec_ inv - lemma_
ref_ serializer_ exec_ inv - lemma_
reference_ parser_ exec_ inv - lemma_
reference_ prepare_ exec_ inv - lemma_
reference_ serializer_ exec_ inv - lemma_
refined_ parser_ exec_ inv - lemma_
refined_ prepare_ exec_ inv - lemma_
refined_ serializer_ exec_ inv - lemma_
repeat_ n_ byte_ len_ exec_ inv - lemma_
repeat_ n_ parser_ exec_ inv - lemma_
repeat_ n_ prepare_ exec_ inv - lemma_
repeat_ n_ serializer_ exec_ inv - lemma_
repeat_ parser_ exec_ inv - lemma_
repeat_ prepare_ exec_ inv - lemma_
repeat_ serializer_ exec_ inv - lemma_
repeat_ till_ end_ parser_ exec_ inv - lemma_
repeat_ till_ end_ slice_ prepare_ exec_ inv - lemma_
repeat_ till_ end_ slice_ serializer_ exec_ inv - lemma_
repeat_ till_ end_ vec_ prepare_ exec_ inv - lemma_
repeat_ till_ end_ vec_ serializer_ exec_ inv - lemma_
star_ parser_ exec_ inv - lemma_
star_ prepare_ exec_ inv - lemma_
star_ serializer_ exec_ inv - lemma_
suffix_ tagged_ parser_ exec_ inv - lemma_
suffix_ tagged_ prepare_ exec_ inv - lemma_
suffix_ tagged_ serializer_ exec_ inv - lemma_
sum_ inl_ parser_ exec_ inv - lemma_
sum_ inl_ prepare_ exec_ inv - lemma_
sum_ inl_ serializer_ exec_ inv - lemma_
sum_ inr_ parser_ exec_ inv - lemma_
sum_ inr_ prepare_ exec_ inv - lemma_
sum_ inr_ serializer_ exec_ inv - lemma_
terminated_ checked_ parser_ exec_ inv - lemma_
terminated_ parser_ exec_ inv - lemma_
terminated_ prepare_ exec_ inv - lemma_
terminated_ serializer_ exec_ inv