Zulip Chat Archive
Stream: new members
Topic: How to use try with `rw [h (by aesop)]`
Malcolm Langfield (Jan 23 2024 at 15:34):
Hi! When using rw [h]
in the case where h
asks for an explicit hypothesis, I sometimes do rw [h (by aesop)]
. However, occasionally the aesop
invocation fails. I expected try rw [h (by aesop)]
to be a no-op if the by aesop
fails. However, it breaks the proof. Does anyone know how to use an inline (by _)
expression to resolve hypotheses in a way which is compatible with try
, or some other way to produce the same desired behavior?
Last updated: May 02 2025 at 03:31 UTC