Struct AlgebraicSignature 

pub struct AlgebraicSignature {
    pub carrier: Sort,
    /* private fields */
}

Backend-agnostic signature for an algebraic structure.

This lets Phase 12 build proof obligations from a reusable semantic model instead of ad-hoc raw strings at each export site.

Fields

carrier: Sort

Implementations

impl AlgebraicSignature

pub fn new(carrier: Sort) -> AlgebraicSignature

pub fn semigroup( carrier: Sort, combine: impl Into<String>, ) -> AlgebraicSignature

pub fn monoid( carrier: Sort, combine: impl Into<String>, identity: impl Into<String>, ) -> AlgebraicSignature

pub fn group( carrier: Sort, combine: impl Into<String>, identity: impl Into<String>, inverse: impl Into<String>, ) -> AlgebraicSignature

pub fn semiring( carrier: Sort, add: impl Into<String>, mul: impl Into<String>, zero: impl Into<String>, one: impl Into<String>, ) -> AlgebraicSignature

pub fn ring( carrier: Sort, add: impl Into<String>, mul: impl Into<String>, zero: impl Into<String>, one: impl Into<String>, neg: impl Into<String>, ) -> AlgebraicSignature

pub fn lattice( carrier: Sort, meet: impl Into<String>, join: impl Into<String>, ) -> AlgebraicSignature

pub fn with_binary( self, role: impl Into<String>, symbol: impl Into<String>, ) -> AlgebraicSignature

pub fn with_unary( self, role: impl Into<String>, symbol: impl Into<String>, ) -> AlgebraicSignature

pub fn with_constant( self, role: impl Into<String>, symbol: impl Into<String>, ) -> AlgebraicSignature

pub fn binary(&self, role: &str) -> Option<&str>

pub fn unary(&self, role: &str) -> Option<&str>

pub fn constant(&self, role: &str) -> Option<&str>

pub fn require_binary(&self, role: &str) -> &str

pub fn require_unary(&self, role: &str) -> &str

pub fn require_constant(&self, role: &str) -> &str

Trait Implementations

impl Clone for AlgebraicSignature

fn clone(&self) -> AlgebraicSignature

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for AlgebraicSignature

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

Formats the value using the given formatter.

impl Eq for AlgebraicSignature

impl PartialEq for AlgebraicSignature

fn eq(&self, other: &AlgebraicSignature) -> 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 AlgebraicSignature