I'm having a little trouble understanding locking and unlocking. Is there a way that I can set an option so that [ffun f x => x] a reduces to f a upon simplification, so I don't have to use the command ffunE every time? Or can I mark a specific finfun as unlockable?
Is this something to do with the phantoms in the first 20 or so lines of the finfun file? I am having trouble making sense of that code
Does unlock
tactic not work?
rewrite ffunE
?
Both unlock and rewrite ffunE work here.
I'm looking for something where I don't have to do this manually, though. Is there a way to get ([ffun x => t] y) to simplify to t[x/y] when the simplification command /= is called?
not for /=
, but rewrite
allows customizable "variants" of /=
that are almost as short
there's even syntax usable inside move
(for the last, see https://coq.zulipchat.com/#narrow/stream/237664-math-comp-users/topic/.E2.9C.94.20Concise.20way.20to.20rewrite.20without.20intro.20.26.20revert.20back.3F/near/297759606)
Last updated: Oct 13 2024 at 01:02 UTC