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