Jason Gross (Nov 15 2022 at 17:18): Jason Gross (Nov 15 2022 at 17:18):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.)
Théo Winterhalter (Nov 15 2022 at 17:23):They might be used in further proofs that rely on functional elimination.
Théo Winterhalter (Nov 15 2022 at 17:24):Could also be a relic of the past.
Matthieu Sozeau (Nov 23 2022 at 12:58):They're probably unnessary now, indeed
Jason Gross (Nov 23 2022 at 13:07):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?
Paolo Giarrusso (Nov 23 2022 at 19:30):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
Matthieu Sozeau (Nov 24 2022 at 11:31):Ah indeed, Paolo might be right here
Last updated: Apr 19 2024 at 00:02 UTC