Stream: MetaCoq

Topic: Moving erased eval to Type


view this post on Zulip 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.

view this post on Zulip Jakob Botsch Nielsen (Sep 23 2020 at 12:55):

@Matthieu Sozeau Ping

view this post on Zulip Matthieu Sozeau (Sep 23 2020 at 12:58):

Yes, that's fine.

view this post on Zulip Matthieu Sozeau (Sep 23 2020 at 12:58):

(The less we have in Prop the better also because MetaCoq doesn't handle Prop <= Type)

view this post on Zulip 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: Aug 11 2022 at 03:02 UTC