From 469ed26e90ef96e44764938c7cdddfb271f272c4 Mon Sep 17 00:00:00 2001
From: Richard Qin <richard.qin.x@gmail.com>
Date: Fri, 3 Apr 2026 14:21:40 +0800
Subject: feat: implement substitution logic and unify/applySubstitution
 functions for term resolution

---
 include/atp/infer/unification.h | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'include/atp/infer/unification.h')

diff --git a/include/atp/infer/unification.h b/include/atp/infer/unification.h
index 7d91aaf..f2ea180 100644
--- a/include/atp/infer/unification.h
+++ b/include/atp/infer/unification.h
@@ -37,4 +37,8 @@ struct UnificationConfig {
 bool unify(const TermBank& bank, TermId t1, TermId t2, Substitution& subst,
            const UnificationConfig& config = {});
 
+/// Apply a substitution to a term recursively, creating new terms in the bank.
+/// Free (unbound) variables are left unchanged.
+TermId applySubstitution(const Substitution& subst, TermId term, TermBank& bank);
+
 }  // namespace atp
-- 
cgit v1.2.3