#check_failure

#check_failure は、エラーが起こった時に成功し、エラーが起こらなければ失敗するコマンドです。エラーが起こるコードを意図的に構成したいときに便利です。

-- 自然数と文字列を足すことはできない
#check_failure 1 + "hello"

-- `1 = 2` を `rfl` で証明することはできない
#check_failure (by rfl : 1 = 2)

-- `1 + 4 = 5` は `contradiction` では示せない
#check_failure (by contradiction : 1 + 4 = 5)