chore: propagate changes

Will Bradley · Will Bradley · commit 186fd46d17f3 · 2025-05-23T22:51:38.000-04:00
diff --git a/LogicFormalization/Chapter2/Section3/Basic.lean b/LogicFormalization/Chapter2/Section3/Basic.lean
@@ -1,4 +1,4 @@
-import LogicFormalization.Chapter2.Section3.Elab
+import LogicFormalization.Chapter2.Section3.Meta
 import Mathlib.Algebra.Group.Hom.Defs
 import Mathlib.Data.Set.Image
 
diff --git a/LogicFormalization/Chapter2/Section3/Meta.lean b/LogicFormalization/Chapter2/Section3/Meta.lean
@@ -112,8 +112,8 @@ elab "#declare_language" lang:ident "{" symbols:langSymbols,* "}" : command => d
   -- declare the inductive types
   let ϝ := lang.getId ++ `ϝ
   let ρ := lang.getId ++ `ρ
-  let fStx ← mkEnum ϝ fSymbols
-  let rStx ← mkEnum ρ rSymbols
+  let fStx ← mkEnum (`Language ++ ϝ) fSymbols
+  let rStx ← mkEnum (`Language ++ ρ) rSymbols
 
   elabInductive {} fStx
   elabInductive {} rStx

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-import LogicFormalization.Chapter2.Section3.Elab`
	`1`	`+import LogicFormalization.Chapter2.Section3.Meta`
`2`	`2`	`import Mathlib.Algebra.Group.Hom.Defs`
`3`	`3`	`import Mathlib.Data.Set.Image`
`4`	`4`