Struct CongruenceTheorem 

pub struct CongruenceTheorem {
    pub fn_name: Name,
    pub num_args: usize,
    pub arg_kinds: Vec<CongrArgKind>,
    pub proof: Option<Expr>,
    pub ty: Option<Expr>,
}

A congruence theorem for a specific function.

Fields

fn_name: Name

The function this theorem is about

num_args: usize

The number of arguments

arg_kinds: Vec<CongrArgKind>

The kind of each argument

proof: Option<Expr>

The proof term (if generated)

ty: Option<Expr>

The type of the congruence lemma

Implementations

impl CongruenceTheorem

pub fn new(fn_name: Name, arg_kinds: Vec<CongrArgKind>) -> Self

Create a new congruence theorem description.

pub fn has_eq_args(&self) -> bool

Check if any argument needs an equality proof.

pub fn num_eq_hypotheses(&self) -> usize

Get the number of equality hypotheses needed.

Trait Implementations

impl Clone for CongruenceTheorem

fn clone(&self) -> CongruenceTheorem

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for CongruenceTheorem

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

Formats the value using the given formatter.