Struct QuotientType 

pub struct QuotientType {
    pub base_type: Expr,
    pub relation: Expr,
    pub quot_type: Expr,
}

A quotient type declaration.

Fields

base_type: Expr

Type being quotiented.

relation: Expr

Equivalence relation.

quot_type: Expr

The quotient type itself.

Implementations

impl QuotientType

pub fn new(base_type: Expr, relation: Expr) -> Self

Create a new quotient type.

pub fn mk_const(&self) -> Expr

Get the mk constant.

pub fn mk_apply(&self, elem: Expr) -> Expr

Apply Quot.mk to an element.

pub fn lift_const(&self) -> Expr

Get the lift constant.

pub fn ind_const(&self) -> Expr

Get the ind constant.

pub fn sound_const(&self) -> Expr

Get the sound constant.

pub fn lift_apply(&self, f: Expr, h: Expr, q: Expr) -> Expr

Apply Quot.lift f h q.

Trait Implementations

impl Clone for QuotientType

fn clone(&self) -> QuotientType

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for QuotientType

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

Formats the value using the given formatter.

impl PartialEq for QuotientType

fn eq(&self, other: &QuotientType) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for QuotientType