- Sponsor
-
Notifications
You must be signed in to change notification settings - Fork 9
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Loading status checks…
set_option
のページの校正
Showing
1 changed file
with
16 additions
and
11 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,20 +1,25 @@ | ||
/- # set_option | ||
`set_option` は、オプションを変更・設定するために使われるコマンドです。 | ||
`set_option option_name value` という構文で使用すれば `option_name` という名前のオプションの値を `value` に設定することができます。使用できる `option_name` は [`#help`](#{root}/Diagnostic/Help.md) コマンドで確認できます。 | ||
`set_option option_name value` という構文で使用すれば `option_name` という名前のオプションの値を `value` に設定することができます。使用できる `option_name` は [`#help`](#{root}/Diagnostic/Help.md) コマンドまたは [Mathlib4 help](https://seasawher.github.io/mathlib4-help/options/) で確認できます。 | ||
有効範囲はその[セクション](./Section.md)の内部またはそのファイルの最後までです。 | ||
有効範囲はその[セクション](#{root}/Declarative/Section.md)の内部またはそのファイルの最後までです。 | ||
-/ | ||
|
||
-- P は命題 | ||
variable (P : Prop) | ||
/-- info: ¬1 + 1 = 2 : Prop -/ | ||
#guard_msgs in #check ¬ (1 + 1 = 2) | ||
|
||
/-- info: ¬P : Prop -/ | ||
#guard_msgs in #check ¬ P | ||
section | ||
|
||
-- 定義された記法を使わないように設定する | ||
set_option pp.notation false | ||
-- 定義された記法を使わないように設定する | ||
set_option pp.notation false | ||
|
||
-- 表示される内容が変わった! | ||
/-- info: Not P : Prop -/ | ||
#guard_msgs in #check ¬ P | ||
-- 表示される内容が変わった! | ||
/-- info: Not (Eq (HAdd.hAdd 1 1) 2) : Prop -/ | ||
#guard_msgs in #check ¬ (1 + 1 = 2) | ||
|
||
end | ||
|
||
-- `section` を抜けると元に戻る | ||
/-- info: ¬1 + 1 = 2 : Prop -/ | ||
#guard_msgs in #check ¬ (1 + 1 = 2) |