Why does MetaCoq use
inspect on recursive calls, e.g., at https://github.com/MetaCoq/metacoq/blob/d702f18ce289530cdd0be3d0ad331cb1ad38f6a0/safechecker/theories/PCUICSafeReduce.v#L486 ? (The equations just get cleared in the obligations.)
They might be used in further proofs that rely on functional elimination.
Could also be a relic of the past.
They're probably unnessary now, indeed
It turns out that if I want to use
where clauses, I seem to need to keep the
inspect for some equations magic to keep working?
where clauses mean the initial match replaces fewer occurrences? A bit like when
destruct t eqn:? can be replaced by more unfolding +
Ah indeed, Paolo might be right here
Last updated: Feb 04 2023 at 03:30 UTC