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