Why is on_ind_body
written to use a mix of match
es and implications? That is, why do we have
(** Projections, if any, are well-typed *)
onProjections :
idecl.(ind_projs) <> [] ->
match idecl.(ind_ctors) return Type with
| [ o ] =>
on_projections mdecl mind i idecl idecl.(ind_indices) o
| _ => False
end;
onIndices :
(* The inductive type respect the variance annotation on polymorphic universes, if any. *)
forall v, ind_variance mdecl = Some v ->
ind_respects_variance Σ mdecl v idecl.(ind_indices)
rather than
(** Projections, if any, are well-typed *)
onProjections :
match idecl.(ind_projs), idecl.(ind_ctors) return Type with
| [], _ => True
| _, [ o ] =>
on_projections mdecl mind i idecl idecl.(ind_indices) o
| _, _ => False
end;
onIndices :
(* The inductive type respect the variance annotation on polymorphic universes, if any. *)
match ind_variance mdecl with
| Some v => ind_respects_variance Σ mdecl v idecl.(ind_indices)
| None => True
end
?
I do not think there is any deep reason for this, I would guess this is a refactoring artefact
Should I submit a PR changing it to use match
es uniformly? (This would work better for me, and I'm happy to spend a bit of time trying to make the change)
I guess that if it makes things easier for you and does not have a major impact on proofs downstream (maybe even makes them nicer), this would be a welcomed PR :)
https://github.com/MetaCoq/metacoq/pull/778
Jason Gross has marked this topic as resolved.
Last updated: May 31 2023 at 04:01 UTC