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`

.

@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: Jun 23 2024 at 01:02 UTC