Struct Unification 

pub struct Unification {
    pub has_unification: bool,
    pub unify_map_1: VarSubstitution,
    pub unify_map_2: VarSubstitution,
}

多值输出：寻找「归一替换」的中间结果

• 🎯使用类似unify_find(t1, t2).apply_to(c1, c2)完成「可变性隔离」

Fields

has_unification: bool

是否能归一

unify_map_1: VarSubstitution

如若归一，归一要换掉的变量映射 @ 词项1

unify_map_2: VarSubstitution

如若归一，归一要换掉的变量映射 @ 词项2

Implementations

impl Unification

pub fn apply_to( &self, parent1: CompoundTermRefMut<'_>, parent2: CompoundTermRefMut<'_>, ) -> bool

重定向到[unify_apply]

• 🚩返回「是否可归一化」
• 🚩【2024-07-09 21:48:43】目前作为一个实用的「链式应用方法」用以替代公开的unifyApply

pub fn apply_to_term(&self, parent1: &mut Term, parent2: &mut Term) -> bool

同Self::apply_to，但允许应用在任何词项中

• 🚩一律返回「是否已归一化」
  • ⚠️对「单个复合词项」仍可能应用归一化失败：与「应用到哪儿」无关

Trait Implementations

impl Clone for Unification

fn clone(&self) -> Unification

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Unification

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

Formats the value using the given formatter.