prod on type level

Stream: new members

[Yakov Pechersky]

If I wanted to define a type synonym such that I could refer to my_matrix (prod m n) α := matrix m n α, what's the way to do that? I'm not sure how to use out_param, or if it is necessary. I get Type errors when I try:

def my_matrix : out_param (prod m n) → Type → Type* :=
λ p ι, matrix p.fst p.snd ι

[Kevin Buzzard]

If p : prod m n then p.fst isn't m.

[Yakov Pechersky]

Ah, right. In Haskell, I can say something like p ~ prod m n. Is this getting close to the dreaded heq?

[Johan Commelin]

You could do def my_matrix (X : Type) (R : Type) := X -> R
and then my_matrix (m \times n) would be the type of -- you know -- m \times n-matrices.

[Johan Commelin]

And with (un)curry, you would be able to move to mathlib's matrices