set_option
set_option
は、オプションを変更・設定するために使われるコマンドです。
set_option option_name value
という構文で使用すれば option_name
という名前のオプションの値を value
に設定することができます。使用できる option_name
は #help
コマンドで確認できます。
有効範囲はその section
の内部またはそのファイルの最後までです。
-- P は命題
variable (P : Prop)
/-- info: ¬P : Prop -/
#guard_msgs in #check ¬ P
-- 定義された記法を使わないように設定する
set_option pp.notation false
-- 表示される内容が変わった!
/-- info: Not P : Prop -/
#guard_msgs in #check ¬ P