## Stream: new members

### Topic: prod on type level

#### Yakov Pechersky (Sep 14 2020 at 20:11):

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 (Sep 14 2020 at 20:28):

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

#### Yakov Pechersky (Sep 14 2020 at 20:32):

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

#### Johan Commelin (Sep 14 2020 at 20:34):

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 (Sep 14 2020 at 20:34):

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

Last updated: May 06 2021 at 22:13 UTC