## Stream: Coq devs & plugin devs

### Topic: case quiz

#### Gaëtan Gilbert (Mar 17 2022 at 13:29):

in context Require Vector., what happens for each check?

Check (fun n (x: Vector.t True (S n)) =>
match x in Vector.t _ (S m) return True with
|Vector.cons _ h _ _ => h
end).

Check (fun n (x: Vector.t True (S n)) =>
match x in Vector.t _ _ return True with
|Vector.cons _ h _ _ => h
end).

Check (fun n (x: Vector.t True (S n)) =>
match x in Vector.t _ _ with
|Vector.cons _ h _ _ => h
end).

Check (fun n (x: Vector.t True (S n)) =>
match x in Vector.t@{} _ _ with
|Vector.cons _ h _ _ => h
end).

Check (fun n (x: Vector.t True (S n)) =>
match x in Vector.t True _ with
|Vector.cons _ h _ _ => h
end).

#### Guillaume Melquiond (Mar 17 2022 at 13:32):

I think the 5th one fails because of the constant argument True. And I suppose (otherwise you would not ask) that the 4th one fails due to the nonsensical universe constraint.

#### Gaëtan Gilbert (Mar 17 2022 at 13:34):

what do you mean nonsensical? Check Vector.t@{}. works fine

#### Guillaume Melquiond (Mar 17 2022 at 13:35):

I mean that it is the same as for the 5th case. Universes have no impact on the matching, so they do not make sense there, same as constant argument.

#### Pierre-Marie Pédrot (Mar 17 2022 at 13:36):

Universes have no impact on the matching

unfortunately that's not really true at least from the kernel point of view

#### Guillaume Melquiond (Mar 17 2022 at 13:37):

Do you mean that it would make sense to match on a universe and then use it in the return clause?

#### Gaëtan Gilbert (Mar 17 2022 at 13:38):

not match on it, but consider how fun x => match x in bool with _ => tt end constraints the type of x, parameters and univs in the in clause could also constraint the discriminee

#### Guillaume Melquiond (Mar 17 2022 at 13:40):

But matching with a pure wildcard is such a degenerate case. Not sure it is worth making things more complicated just for it.

#### Gaëtan Gilbert (Mar 17 2022 at 13:42):

the data is there in the kernel so we should have a way to print it. then it's natural to also parse it.

#### Guillaume Melquiond (Mar 17 2022 at 13:44):

Actually, I am surprised it is there in the first place. I would have expected only the binders to appear in the kernel in clause, not the full inductive type.

#### Pierre-Marie Pédrot (Mar 17 2022 at 13:57):

About the return clause, the kernel sees the instance, the parameters and that's about it (the names are also there but not relevant).

Last updated: Nov 29 2023 at 18:01 UTC