register_option

register_option は、オプションを自作するためのコマンドです。自作したオプションは set_option から設定できるようになります。

注意

このページの内容は ボタンから Lean 4 Web で実行することができません。

使用例

たとえば、RegisterOptionLib.lean というファイルを作成して、以下のように記述したとします。

-- RegisrerOptionLib.lean の内容
import Lean

open Lean

register_option greeting : String := {
  defValue := "Hello World"
  descr := "just a friendly greeting"
}

このファイルを読み込めば、greeting というオプションを使用することができます。たとえば、以下のように使用することができます。

import LeanByExample.Declarative.RegisterOptionLib

open Lean in

elab "#greet" : command => do
  let opts ← getOptions
  logInfo s!"{opts.get greeting.name greeting.defValue}"

-- デフォルト値が表示される
/- info: Hello World -/
#greet

-- オプションを設定すると
set_option greeting "Hi there"

-- 表示も変更される
/- info: Hi there -/
#greet

設定したオプションを活用する例は、Linter のページを参照のこと。