Jason Gross (Oct 21 2022 at 14:36): 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
Jason Gross (Oct 21 2022 at 14:43):And it seems that local_entry is missing the type of the let binders?
Jason Gross (Oct 21 2022 at 14:45):And it's also missing relevance information
Jason Gross (Oct 21 2022 at 14:45):Is mutual_inductive_entry correct in the face of SProp let-binders?
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
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.
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: May 31 2023 at 03:30 UTC