where is better to put the type dependency info?

Stream: lean4

[Gabriel gomez]

Which one is better?

  inductive Pair (x: Type) (p q : x -> Type)   where
  | mk : {a: x} -> p a ->  q a -> Pair x p q

or

  inductive Pair2 (x: Type) (a: x) (p q : x -> Type)   where
  | mk : p a ->  q a -> Pair2 x a p q

[Gabriel gomez]

I suppose the difference is option 2 doesn't allow to pattern match on value (a :x) and option 1 allow us to do it.

[Henrik Böving]

sure you can still pattern match on it, the argument is still down in the mk as an auto implicit, it is just that the result type changed. But I don't see a reason to index a pair by this parameter value in this way from the top of my head.

[Gabriel gomez]

Well, I was translating bad some haskell code from the paper: http://strictlypositive.org/CJ.pdf
I fixed my translation and it's compiling at least. I'll continue checking the paper.

[Kyle Miller]

If I understand the very little of the paper that I read correctly, the most accurate translation would be

inductive Pair3 (x : Type) (p q : x -> Type) (a: x) where
  | mk : p a ->  q a -> Pair3 x p q a

since then you have Pair3 x p q : x -> Type. (It probably wouldn't hurt to make x implicit.)

[Kyle Miller]

There's a big difference between Pair and Pair2 by the way. Pair2 x a p q can be thought of as just those terms of Pair x p q of the form Pair.mk {a} _ _ (ones with a specific value of a).