Skip to main content

lemma_disjoint_const

vest_lib::combinators::disjoint

Function lemma_disjoint_const 

Source 
pub broadcast proof fn lemma_disjoint_const<Inner: SpecParser>(
    tag1: Const<Inner, Inner::PVal>,
    tag2: Const<Inner, Inner::PVal>,
)
Expand description
requires
tag1.0 == tag2.0,
tag1.1 != tag2.1,
ensures
#[trigger] disjoint_domains(tag1, tag2),

Two Const parsers with the same inner parser but different values are disjoint.