1.12. Control flow

sorry

The sorry tactic is a temporary placeholder for an incomplete tactic proof, closing the main goal using exact sorry.

This is intended for stubbing-out incomplete parts of a proof while still having a syntactically correct proof skeleton. Lean will give a warning whenever a proof uses sorry, so you aren't likely to miss it, but you can double check if a theorem depends on sorry by looking for sorryAx in the output of the #print axioms my_thm command, the axiom used by the implementation of sorry.

done

done succeeds iff there are no remaining goals.

checkpoint

checkpoint tac acts the same as tac, but it caches the input and output of tac, and if the file is re-elaborated and the input matches, the tactic is not re-run and its effects are reapplied to the state. This is useful for improving responsiveness when working on a long tactic proof, by wrapping expensive tactics with checkpoint.

See the save tactic, which may be more convenient to use.

(TODO: do this automatically and transparently so that users don't have to use this combinator explicitly.)

save

save is defined to be the same as skip, but the elaborator has special handling for occurrences of save in tactic scripts and will transform by tac1; save; tac2 to by (checkpoint tac1); tac2, meaning that the effect of tac1 will be cached and replayed. This is useful for improving responsiveness when working on a long tactic proof, by using save after expensive tactics.

(TODO: do this automatically and transparently so that users don't have to use this combinator explicitly.)

stop

stop is a helper tactic for "discarding" the rest of a proof: it is defined as repeat sorry. It is useful when working on the middle of a complex proofs, and less messy than commenting the remainder of the proof.