How does one use where finally in the creation of defs?
On Zulip, #general > Block at end of `def` for solving holes in tactic mode, this feature was vaguely remembered by a user, but they didn't recall the syntax where finally. Several members of the community had no knowledge feature at all.
The reference manual should document the existence of this feature and basic usage, as well as any possible side effects of which the user should be aware (e.g., how is final term constructed? presumably not with have, but maybe haveI?).
How does one use
where finallyin the creation ofdefs?On Zulip, #general > Block at end of `def` for solving holes in tactic mode, this feature was vaguely remembered by a user, but they didn't recall the syntax
where finally. Several members of the community had no knowledge feature at all.The reference manual should document the existence of this feature and basic usage, as well as any possible side effects of which the user should be aware (e.g., how is final term constructed? presumably not with
have, but maybehaveI?).