Skip to content

Commit

Permalink
fix failing Comp test
Browse files Browse the repository at this point in the history
By reviving some instances from deleted file
  • Loading branch information
alexkeizer committed Dec 4, 2024
1 parent 08c6879 commit 541ff84
Show file tree
Hide file tree
Showing 2 changed files with 24 additions and 6 deletions.
15 changes: 9 additions & 6 deletions Qpf/Macro/Comp.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
15 changes: 15 additions & 0 deletions Qpf/Qpf/Multivariate/Basic.lean
Original file line number Diff line number Diff line change
@@ -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

0 comments on commit 541ff84

Please sign in to comment.