diff --git a/Qpf/Macro/Data.lean b/Qpf/Macro/Data.lean index 299492d..fde35ab 100644 --- a/Qpf/Macro/Data.lean +++ b/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