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).
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.
what do you mean nonsensical? Check Vector.t@{}.
works fine
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.
Universes have no impact on the matching
unfortunately that's not really true at least from the kernel point of view
Do you mean that it would make sense to match on a universe and then use it in the return
clause?
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
But matching with a pure wildcard is such a degenerate case. Not sure it is worth making things more complicated just for it.
the data is there in the kernel so we should have a way to print it. then it's natural to also parse it.
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.
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: Oct 13 2024 at 01:02 UTC