Struct EFlintIteratorOperator

pub struct EFlintIteratorOperator;

Defines identifiers for eFLINT operators that can (only) be used in iterator expressions.

Note that these are only Foreach, Forall and Exists. Other operators -like Count and Sum- do not quantify, but rather take a Foreach to do the quantification for them.

For non-iterator operators, see EFlintOperator.

Implementations

impl EFlintIteratorOperator

pub const EXISTS: &str = "EXISTS"

Takes an instance pattern and checks if at least one of those generated is true.

pub const FORALL: &str = "FORALL"

Takes an instance pattern and checks if all of those generated are true.

pub const FOREACH: &str = "FOREACH"

Foreach generates an instance expression based on the given instance pattern.

pub const fn all() -> &'static [&'static str]

Returns a list of all the iterator operators in eFLINT.

Returns

A static slice with all iterator operators.

pub fn kind(op: &str) -> ExpressionKind

Trait Implementations

impl Clone for EFlintIteratorOperator

fn clone(&self) -> EFlintIteratorOperator

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for EFlintIteratorOperator

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

Formats the value using the given formatter.

impl Copy for EFlintIteratorOperator