try

try は，失敗するかもしれないタクティクをエラーにすることなく実行します．try で指定されたタクティクが成功した場合は try なしの場合と変わりませんが，失敗した場合は try 実行前の状態に戻ります．

import Aesop -- `aesop` を使用するため

variable (P Q : Prop)

example : (P → Q) → (¬ Q → ¬ P) := by
  -- `assumption` は通らないが，エラーにならない
  try assumption

  try
    -- `aesop` が通り，証明が終了する
    aesop
    done

    -- 強制的に失敗させる
    fail

  -- `try` 実行前の状態に戻る
  show (P → Q) → ¬Q → ¬P

  aesop