Update Qpf/Macro/Data/Constructors.lean

Co-authored-by: Atticus Kuhn <[email protected]>
alexkeizer · Aug 16, 2024 · 89b86d2 · 89b86d2
1 parent c6ee24d
commit 89b86d2
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Qpf/Macro/Data/Constructors.lean b/Qpf/Macro/Data/Constructors.lean
@@ -71,6 +71,6 @@ def mkConstructors (view : DataView) (shape : Name) : CommandElabM Unit := do
   let explicit ← view.getExplicitExpectedType
   let nameGen := (·.declName.replacePrefix (←getCurrNamespace) .anonymous)
 
-  mkConstructorsWithNameAndType view shape nameGen explicit explicit #[]
+  mkConstructorsWithNameAndType view shape nameGen explicit explicit (binders := #[])
 
 end Data.Command