Jason Gross (Oct 26 2022 at 14:34): Jason Gross (Oct 26 2022 at 14:34):Why is on_ind_body written to use a mix of matches 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
?
Meven Lennon-Bertrand (Oct 26 2022 at 14:41):I do not think there is any deep reason for this, I would guess this is a refactoring artefact
Jason Gross (Oct 26 2022 at 14:46):Should I submit a PR changing it to use matches uniformly? (This would work better for me, and I'm happy to spend a bit of time trying to make the change)
Meven Lennon-Bertrand (Oct 26 2022 at 14:49):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 :)
Jason Gross (Oct 26 2022 at 17:10):https://github.com/MetaCoq/metacoq/pull/778
Notification Bot (Nov 07 2022 at 23:10):Jason Gross has marked this topic as resolved.
Last updated: May 31 2023 at 04:01 UTC