feat: add the ability to access the uncurried base

Qpf/Macro/Data.lean

@@ -412,7 +412,8 @@ 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 baseIdent ← addSuffixToDeclIdent view.declId "Base"
+  let baseIdExt ← addSuffixToDeclIdent view.declId "Base"
+  let baseIdent ← addSuffixToDeclIdent baseIdExt "Uncurried"
   let baseFunctorIdent ← addSuffixToDeclIdent baseIdent "instMvFunctor"
   let baseQPFIdent ← addSuffixToDeclIdent baseIdent "instQPF"
 
@@ -430,6 +431,9 @@ 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
+
     instance $baseFunctorIdent:ident : MvFunctor ($baseApplied) := $functor
     instance $baseQPFIdent:ident : MvQPF ($baseApplied) := $q