Update Qpf/Macro/Data.lean

Co-authored-by: Alex Keizer <alex@keizer.dev>
alexkeizer · Aug 17, 2024 · 633e2c0 · 633e2c0
1 parent 3a2949e
commit 633e2c0
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Qpf/Macro/Data.lean b/Qpf/Macro/Data.lean
@@ -431,8 +431,8 @@ def mkType (view : DataView) (base : Term × Term × Term) : CommandElabM Unit :
     abbrev $baseIdent:ident $view.deadBinders:bracketedBinder* : TypeFun $(quote <| arity + 1) :=
       $base
 
-    abbrev $baseIdExt $view.deadBinders:bracketedBinder*
-      := TypeFun.curried $baseApplied
+    abbrev $baseIdExt $view.deadBinders:bracketedBinder* := 
+      TypeFun.curried $baseApplied
 
     instance $baseFunctorIdent:ident : MvFunctor ($baseApplied) := $functor
     instance $baseQPFIdent:ident : MvQPF ($baseApplied) := $q