Promote Substitution to its own top-level module

WegmannDavid · claude · WegmannDavid · commit 23d7a87ac6b8 · 2026-05-09T02:20:50.000+02:00
The `HasVars`/`HasSubst` typeclasses are independent of unification —
keeping them under `Unification/` understated their general role.
Move `Unification/Substitution.lean` to `Substitution/Basic.lean`
and update the two import sites (`LambdaLab.lean`,
`Unification/Term.lean`).

Co-Authored-By: Claude Opus 4.7 (1M context) &lt;noreply@anthropic.com&gt;
diff --git a/LambdaLab.lean b/LambdaLab.lean
@@ -29,7 +29,7 @@ import LambdaLab.Stlc.Named.Lang
 import LambdaLab.Language.Basic
 import LambdaLab.Language.Parser
 import LambdaLab.Language.Check
-import LambdaLab.Unification.Substitution
+import LambdaLab.Substitution.Basic
 import LambdaLab.Unification.Term
 import LambdaLab.Unification.Bridge
 import LambdaLab.Unification.Measure
diff --git a/LambdaLab/Substitution/Basic.lean b/LambdaLab/Substitution/Basic.lean
diff --git a/LambdaLab/Unification/Term.lean b/LambdaLab/Unification/Term.lean
@@ -1,4 +1,4 @@
-import LambdaLab.Unification.Substitution
+import LambdaLab.Substitution.Basic
 
 /-! # Generic free term algebra (Fin-function args, no typeclass)
 

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-import LambdaLab.Unification.Substitution`
	`1`	`+import LambdaLab.Substitution.Basic`
`2`	`2`
`3`	`3`	`/-! # Generic free term algebra (Fin-function args, no typeclass)`
`4`	`4`