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