Skip to main content

lemma_disjoint_void_right

vest_lib::combinators::disjoint

Function lemma_disjoint_void_right 

Source 
pub broadcast proof fn lemma_disjoint_void_right<Other: SpecParser>(other: Other, void: Void)
Expand description
ensures
#[trigger] disjoint_domains(other, void),

Every parser is disjoint from Void.