The qpf macro currently is not able to handle sigma types. See the following examples. There already exists a MvQPF.Sigma but it has not been hooked up yet.
qpf F₁ A B := A × B -- works, `Prod`
qpf F₂ A := (C : Type) × (C -> A) -- fails
qpf F₃ A := (i : Nat) × (A × Fin i) -- fails
The
qpfmacro currently is not able to handle sigma types. See the following examples. There already exists aMvQPF.Sigmabut it has not been hooked up yet.