Zulip Chat Archive

Stream: new members

Topic: prod on type level


view this post on Zulip 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 ι

view this post on Zulip Kevin Buzzard (Sep 14 2020 at 20:28):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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