Struct Unifier 

pub struct Unifier { /* private fields */ }

Unification engine with constraint solving

Implementations

impl Unifier

pub fn new() -> Self

Create a new unifier

pub fn add_constraint(&mut self, constraint: Constraint)

Add a constraint to the queue

pub fn unify(&mut self, t1: TermId, t2: TermId)

Unify two terms

pub fn declare_mvar(&mut self, mvar: MetaVarId, ty: TermId)

Declare a metavariable with its type

pub fn solve( &mut self, arena: &mut Arena, env: &Environment, ctx: &Context, ) -> Result<()>

Solve all pending constraints

pub fn substitution(&self) -> &Substitution

Get the current substitution

pub fn is_solved(&self) -> bool

Check if all constraints are solved

pub fn num_constraints(&self) -> usize

Get the number of pending constraints

Trait Implementations

impl Default for Unifier

fn default() -> Self

Returns the “default value” for a type.