hygine というオプションを紹介する

[Seasawher]

-- マクロ衛生とはなんぞやという例
section

macro "const" e:term : term => `(fun x => $e)

def x : Nat := 42
def y : Nat := 42

#guard (const x) 0 = 42
#guard (const y) 0 = 42

-- マクロ衛生を保つ機能を無効にする
set_option hygiene false

macro "const'" e:term : term => `(fun x => $e)

-- 引数の値が同じでも、識別子の名前によって値が変わるようになる
#guard (const' x) 0 = 0
#guard (const' y) 0 = 42

end