Jakob Botsch Nielsen (Sep 07 2020 at 13:09): Jakob Botsch Nielsen (Sep 07 2020 at 13:09):Are there any blockers to move erased eval from Prop to Type? I have some proofs I want to do by induction in the derivation length which is very annoying to define since eval lives in Prop. Would a PR that moved this to Type be accepted (assuming I fix proofs)? It seems the other evaluation relations already live in Type.
Jakob Botsch Nielsen (Sep 23 2020 at 12:55):@Matthieu Sozeau Ping
Matthieu Sozeau (Sep 23 2020 at 12:58):Yes, that's fine.
Matthieu Sozeau (Sep 23 2020 at 12:58):(The less we have in Prop the better also because MetaCoq doesn't handle Prop <= Type)
Jakob Botsch Nielsen (Sep 23 2020 at 13:00):Ok, I will do that. I will probably also submit some theory about deriviations then, I think we should have uniqueness of derivations starting with the same term now that the inequality proof is gone from eval_fix_value, so I will try to prove this (it simplifies some stuff in our development)
Last updated: Apr 19 2024 at 23:02 UTC