Stream: MetaCoq

Topic: Parametericity translation


view this post on Zulip Matthieu Sozeau (Jul 05 2020 at 13:50):

As was revealed during the Coq Workshop talk of Bohdan Liesnikov, the current param_original.v translation is buggy w.r.t universes and also fix-case, and requires some post-processing for their use case. @Cyril Cohen had a PR implementing fixes to it, we should integrate it.

view this post on Zulip Yannick Forster (Jul 05 2020 at 13:54):

I think @Marcel Ullrich has a concrete example which fails, namely applying the translation to sigT

view this post on Zulip Cyril Cohen (Jul 05 2020 at 13:55):

Matthieu Sozeau said:

As was revealed during the Coq Workshop talk of Bohdan Liesnikov, the current param_original.v translation is buggy w.r.t universes and also fix-case, and requires some post-processing for their use case. Cyril Cohen had a PR implementing fixes to it, we should integrate it.

https://github.com/MetaCoq/metacoq/pull/94/files

view this post on Zulip Marcel Ullrich (Jul 05 2020 at 14:31):

SigT seems to work, my mistake was at another point.
But certain types like roseTree have errors.
Inductive roseTree := tree (h:list roseTree).


Last updated: Aug 11 2022 at 02:03 UTC