Struct ForallFactWithIff 

pub struct ForallFactWithIff {
    pub forall_fact: ForallFact,
    pub iff_facts: Vec<ExistOrAndChainAtomicFact>,
    pub line_file: LineFile,
}

Fields

forall_fact: ForallFact

iff_facts: Vec<ExistOrAndChainAtomicFact>

line_file: LineFile

Implementations

impl ForallFactWithIff

pub fn new( forall_fact: ForallFact, iff_facts: Vec<ExistOrAndChainAtomicFact>, line_file: LineFile, ) -> Result<Self, RuntimeError>

impl ForallFactWithIff

pub fn to_two_forall_facts( &self, ) -> Result<(ForallFact, ForallFact), RuntimeError>

impl ForallFactWithIff

pub fn error_messages_if_forall_param_missing_in_forall_then_clause( &self, ) -> Vec<(usize, String)>

Only checks the embedded ForallFact’s then_facts (not iff_facts).

impl ForallFactWithIff

pub fn to_latex_string(&self) -> String

Trait Implementations

impl Clone for ForallFactWithIff

fn clone(&self) -> ForallFactWithIff

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Display for ForallFactWithIff

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl From<ForallFactWithIff> for Fact

fn from(forall_fact_with_iff: ForallFactWithIff) -> Self

Converts to this type from the input type.