diff --git a/Qpf/Macro/Comp.lean b/Qpf/Macro/Comp.lean index f913e56..9ce8c42 100644 --- a/Qpf/Macro/Comp.lean +++ b/Qpf/Macro/Comp.lean @@ -310,14 +310,17 @@ def elabQpfCompositionBody (view: QpfCompositionBodyView) : res.F.check res.qpf.check - withOptions (fun opt => opt.insert `pp.explicit true) <| do + let (F, qpf) ← withOptions (fun opt => opt.insert `pp.explicit true) <| do let F ← delab res.F let qpf ← delab res.qpf - - withQPFTraceNode "results …" <| do - trace[QPF] "Functor := {F}" - trace[QPF] "MvQPF instance := {qpf}" - return ⟨F, qpf⟩ + pure (F, qpf) + + withQPFTraceNode "results …" <| do + trace[QPF] "Functor (expr) := {res.F}" + trace[QPF] "Functor (stx) := {F}" + trace[QPF] "MvQPF (expr) := {res.qpf}" + trace[QPF] "MvQPF (stx) := {qpf}" + return ⟨F, qpf⟩ structure QpfCompositionView where diff --git a/Qpf/Qpf/Multivariate/Basic.lean b/Qpf/Qpf/Multivariate/Basic.lean new file mode 100644 index 0000000..b28c324 --- /dev/null +++ b/Qpf/Qpf/Multivariate/Basic.lean @@ -0,0 +1,15 @@ +import Mathlib.Data.QPF.Multivariate.Basic +import Qpf.Util.TypeFun + +namespace MvQPF +variable {n} {F : TypeFun n} + +instance instMvFunctor_ofCurried_curried [f : MvFunctor F] : + MvFunctor <| TypeFun.ofCurried <| F.curried := + TypeFun.ofCurried_curried_involution ▸ f + +instance instQPF_ofCurried_curried [q : MvQPF F] : + MvQPF <| TypeFun.ofCurried <| F.curried := + TypeFun.ofCurried_curried_involution ▸ q + +end MvQPF