Stream: MetaCoq

Topic: ✔ `on_ind_body`


view this post on Zulip 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

?

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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 :)

view this post on Zulip Jason Gross (Oct 26 2022 at 17:10):

https://github.com/MetaCoq/metacoq/pull/778

view this post on Zulip 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