chore: clean up ws

alexkeizer · Aug 15, 2024 · f24ad61 · f24ad61
1 parent 82ba66e
commit f24ad61
Showing 1 changed file with 4 additions and 5 deletions.
diff --git a/Qpf/Macro/Data.lean b/Qpf/Macro/Data.lean
@@ -411,11 +411,11 @@ def isPolynomial (view : DataView) (F: Term) : CommandElabM (Option Term) := do
 -/
 def mkType (view : DataView) (base : Term × Term × Term) : CommandElabM Unit := do
   trace[QPF] "mkType"
-  let uncurriedIdent   ← addSuffixToDeclIdent view.declId "Uncurried"
-  let baseIdExt        ← addSuffixToDeclIdent view.declId "Base"
-  let baseIdent        ← addSuffixToDeclIdent baseIdExt "Uncurried"
+  let uncurriedIdent ← addSuffixToDeclIdent view.declId "Uncurried"
+  let baseIdExt ← addSuffixToDeclIdent view.declId "Base"
+  let baseIdent ← addSuffixToDeclIdent baseIdExt "Uncurried"
   let baseFunctorIdent ← addSuffixToDeclIdent baseIdent "instMvFunctor"
-  let baseQPFIdent     ← addSuffixToDeclIdent baseIdent "instQPF"
+  let baseQPFIdent ← addSuffixToDeclIdent baseIdent "instQPF"
 
   let deadBinderNamedArgs ← view.deadBinderNames.mapM fun n =>
         `(namedArgument| ($n:ident := $n:term))
@@ -483,5 +483,4 @@ def elabData : CommandElab := fun stx => do
   try genRecursors view shape
   catch e => trace[QPF] (← e.toMessageData.toString)
 
-
 end Data.Command