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
@Matthieu Sozeau Ping
Yes, that's fine.
(The less we have in Prop the better also because MetaCoq doesn't handle Prop <= Type)
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: May 31 2023 at 10:01 UTC