MCPcopy Create free account
hub / github.com/agenticsorg/lean-agentic / unify

Method unify

lean-agentic/src/unification.rs:95–97  ·  view source on GitHub ↗

Unify two terms

(&mut self, t1: TermId, t2: TermId)

Source from the content-addressed store, hash-verified

93
94 /// Unify two terms
95 pub fn unify(&mut self, t1: TermId, t2: TermId) {
96 self.add_constraint(Constraint::Unify(t1, t2));
97 }
98
99 /// Declare a metavariable with its type
100 pub fn declare_mvar(&mut self, mvar: MetaVarId, ty: TermId) {

Callers 5

synthMethod · 0.80
checkMethod · 0.80
test_basic_unificationFunction · 0.80
test_occurs_checkFunction · 0.80

Calls 1

add_constraintMethod · 0.80

Tested by 3

test_basic_unificationFunction · 0.64
test_occurs_checkFunction · 0.64