local
local
はコマンドをその section
の内部でだけ有効にするための修飾子です。
section foo
-- local を付けて新しい記法を定義
local notation " succ' " => Nat.succ
-- section の中では使用できる
#check succ'
end foo
-- section を抜けると使えなくなる
#check_failure succ'
section foo
-- 同じ名前の section を再度開いても使えない
#check_failure succ'
end foo
コマンドのスコープを namespace
の内部に限定するのにも使えます。ただし、下記のコードで示しているように、local
で修飾したコマンドの効果は同じ名前空間の中で永続するのではなく、end
でその名前空間が閉じられたときに消失します。
namespace hoge
-- local を付けて新しい記法を定義
local notation " succ' " => Nat.succ
-- 定義した namespace の中では使用できる
#check succ' 2
end hoge
-- namespace の外では使用できない
#check_failure succ' 2
-- 再び同じ名前の namespace をオープンする
namespace hoge
-- 使用できない!
#check_failure succ'
end hoge
修飾可能なコマンド
local
で有効範囲を限定できるコマンドには、次のようなものがあります。
elab
,elab_rules
infix
,infil
,infixr
macro
,macro_rules
notation
postfix
prefix
instance
syntax
- などなど
リストの全体は、local
の後に修飾できないコマンドを続けたときのエラーメッセージで確認できます。
open Lean Parser in
/-- `s : String` をパースして `Syntax` の項を得る。`cat` は構文カテゴリ。-/
def parse (cat : Name) (s : String) : MetaM Syntax := do
ofExcept <| runParserCategory (← getEnv) cat s
-- `def` は有効範囲を制限できないのでエラーになる
/--
error: <input>:1:6: expected 'binder_predicate', 'builtin_dsimproc', 'builtin_simproc', 'dsimproc',
'elab', 'elab_rules', 'infix', 'infixl', 'infixr', 'instance', 'macro', 'macro_rules',
'notation', 'postfix', 'prefix', 'simproc', 'syntax' or 'unif_hint'
-/
#guard_msgs in
run_meta parse `command "local def"
数が多いためすべての例を挙げることはしませんが、いくつか紹介します。たとえば instance
の場合、local
を付けて登録したインスタンスがその section
の内部限定になります。
inductive MyNat : Type where
| zero : MyNat
| succ : MyNat → MyNat
section
-- local を付けてインスタンスを定義
local instance : OfNat MyNat 0 where
ofNat := MyNat.zero
-- その section の中では使用できる
#check (0 : MyNat)
end
-- section を抜けると使えなくなる
#check_failure (0 : MyNat)
属性に対する local
属性付与の効果範囲を限定するためには、attribute
コマンドを local
で修飾するのではなく、attribute
コマンドの中で local
を使います。
def MyNat.add (n m : MyNat) : MyNat :=
match m with
| zero => n
| succ m => succ (MyNat.add n m)
theorem MyNat.zero_add (n : MyNat) : MyNat.add .zero n = n := by
induction n with
| zero => rfl
| succ n ih => simp [MyNat.add, ih]
section
-- [simp] 属性をローカルに付与する
attribute [local simp] MyNat.zero_add
-- その section の中では使用できる
#check (by simp : MyNat.add .zero .zero = .zero)
end
-- section を抜けると simp 補題が利用できなくなる
#check_failure (by simp : MyNat.add .zero .zero = .zero)
構文的な性質
local
と scoped
はともに構文的には attrKind
に相当します。
/-- 例示のための意味のないコマンド -/
macro attrKind "#greet " : command => `(#eval "hello")
-- パース出来るので、`local` と `scoped` は同じカテゴリに属する
local #greet
scoped #greet