Stream: MetaCoq

Topic: mutual_inductive_entry


view this post on Zulip Jason Gross (Oct 21 2022 at 14:36):

Is there a way to translate PCUICAst.mutual_inductive_entry to Template.Ast.mutual_inductive_entry? The former is missing mind_entry_variance, and I don't see an obvious way to turn mind_entry_params : list (ident × local_entry) into context

view this post on Zulip Jason Gross (Oct 21 2022 at 14:43):

And it seems that local_entry is missing the type of the let binders?

view this post on Zulip Jason Gross (Oct 21 2022 at 14:45):

And it's also missing relevance information

view this post on Zulip Jason Gross (Oct 21 2022 at 14:45):

Is mutual_inductive_entry correct in the face of SProp let-binders?

view this post on Zulip Meven Lennon-Bertrand (Oct 26 2022 at 13:35):

I am not very familiar with that part of the code base so I can't answer for sure… But at least I know that for now SProp is still very much in the making: some things are there, but we do not have the irrelevance conversion rule, so basically the relevance information is currently unused, and so might be buggy in some places

view this post on Zulip Théo Winterhalter (Oct 26 2022 at 13:41):

@Yann Leray has been working on SProp, but I don't know if everything he did was merged.

view this post on Zulip Meven Lennon-Bertrand (Oct 26 2022 at 13:42):

As far as I know, this still lives in an independent branch, and there is some work remaining before it can be merged


Last updated: Jan 30 2023 at 18:04 UTC