Documentation

CustomPrelude.Linter.Syntax.SelectorTry

linter.fugue.selectorTry #

all: try tac — and every other selector over a bare try (1-3: try tac, all_goals try tac) — runs tac under try, so a goal where tac fails is silently left untouched and the proof no longer records which goals the selector closed. Name the goals the tactic applies to (1,3: tac), or drop the try and the selector both if it closes them all.