Stream: MetaCoq

Topic: inspect on recursive calls


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

view this post on Zulip Théo Winterhalter (Nov 15 2022 at 17:23):

They might be used in further proofs that rely on functional elimination.

view this post on Zulip Théo Winterhalter (Nov 15 2022 at 17:24):

Could also be a relic of the past.

view this post on Zulip Matthieu Sozeau (Nov 23 2022 at 12:58):

They're probably unnessary now, indeed

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

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

view this post on Zulip Matthieu Sozeau (Nov 24 2022 at 11:31):

Ah indeed, Paolo might be right here


Last updated: Feb 04 2023 at 03:30 UTC