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?

maybe `where`

clauses mean the initial match replaces fewer occurrences? A bit like when `destruct t eqn:?`

can be replaced by more unfolding + `destruct t`

Ah indeed, Paolo might be right here

Last updated: Feb 04 2023 at 03:30 UTC