Skip to main content

lemma_alt_parser_congruence

vest_lib::combinators::congruence

Function lemma_alt_parser_congruence 

Source 
pub broadcast proof fn lemma_alt_parser_congruence<const NONDETERMINISTIC: bool, A1: SpecParser, A2: SpecParser<PVal = A1::PVal>, B1: SpecParser<PVal = A1::PVal>, B2: SpecParser<PVal = A1::PVal>>(
    a1: A1,
    a2: A2,
    b1: B1,
    b2: B2,
)
Expand description
requires
parser_congruent(a1, a2),
parser_congruent(b1, b2),
ensures
#[trigger]
parser_congruent(
    Alt::<A1, B1, NONDETERMINISTIC>(a1, b1),
    Alt::<A2, B2, NONDETERMINISTIC>(a2, b2),
),