Merge branch 'codef-2' into codef-3-deepThunk

alexkeizer · Aug 8, 2024 · d8be71e · d8be71e
2 parents 5befbab + 432649e
commit d8be71e
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 9 deletions.
diff --git a/Qpf/Macro/Data.lean b/Qpf/Macro/Data.lean
@@ -65,7 +65,7 @@ open Elab.Term (TermElabM)
 
 
 def CtorView.declReplacePrefix (pref new_pref : Name) (ctor: CtorView) : CtorView :=
-  let declName := Name.replacePrefix ctor.declName pref new_pref 
+  let declName := ctor.declName.replacePrefix pref new_pref
   {
     declName,
     ref := ctor.ref

diff --git a/Qpf/Macro/Data/Constructors.lean b/Qpf/Macro/Data/Constructors.lean
@@ -25,21 +25,19 @@ def mkConstructorsWithNameAndType
     trace[QPF] "mkConstructors\n{ctor.declName} : {ctor.type?}"
     let n_args := (ctor.type?.map countConstructorArgs).getD 0
 
-    let args ← (List.range n_args).mapM fun _ =>
-      do pure <| mkIdent <|← Elab.Term.mkFreshBinderName
-    let args := args.toArray
+    let args := (← (List.range n_args).mapM
+      fun _ => do pure <| mkIdent <|← Elab.Term.mkFreshBinderName).toArray
 
-    let mk := mkIdent ((DataCommand.fixOrCofix view.command).getId ++ `mk)
+    let pointConstructor := mkIdent ((DataCommand.fixOrCofix view.command).getId ++ `mk)
     let shapeCtor := mkIdent <| Name.replacePrefix ctor.declName view.declName shape
     trace[QPF] "shapeCtor = {shapeCtor}"
 
 
 
-    let body := if n_args = 0 then
-        `($mk $shapeCtor)
+    let body ← if n_args = 0 then
+        `($pointConstructor $shapeCtor)
       else
-        `(fun $args:ident* => $mk ($shapeCtor $args:ident*))
-    let body ← body
+        `(fun $args:ident* => $pointConstructor ($shapeCtor $args:ident*))
 
     let recType := view.getExpectedType
     let forms := RecursionForm.extract ctor recType