From 633e2c06eef9790fbfdeb8f04949472010d3394a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?William=20S=C3=B8rensen?= <47296141+Equilibris@users.noreply.github.com> Date: Sat, 17 Aug 2024 13:27:31 +0200 Subject: [PATCH] Update Qpf/Macro/Data.lean Co-authored-by: Alex Keizer --- Qpf/Macro/Data.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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