section

section は、スコープを区切るためのコマンドです。以下のコマンドのスコープを区切ることができます。

section で開いたスコープは end で閉じることができますが、省略することもでき、その場合はそのファイルの終わりまでがスコープとなります。

なお以下の例ではセクションの中をインデントしていますが、インデントするのは一般的なコード整形ルールではありません。

次は variable のスコープを区切る例です。

section
  variable (a : Type)

  -- 宣言したので有効
  #check a
end

-- `section` の外に出ると無効になる
#check_failure a

次は open のスコープを区切る例です。

section
  open Classical

  -- open されているのでアクセスできる
  #check choice
end

-- スコープが終わると無効になる
#check_failure choice

次は set_option のスコープを区切る例です。

section
  set_option autoImplicit true

  -- α が暗黙引数になる
  def nilList : List α := []
end

-- スコープが終わると無効になり、α が未定義だというエラーになる
/-- error: unknown identifier 'α' -/
#guard_msgs in def nilList' : List α := []

次は local のスコープを区切る例です。local は、セクション内部でだけ有効なインスタンスなどを生成します。

section
  -- Nat の inhabited インスタンスを上書きする
  local instance : Inhabited Nat := ⟨1⟩

  -- 上記のインスタンスが有効
  #guard (default : Nat) = 1
end

-- スコープが終わると上記のインスタンスが無効になる
#guard (default : Nat) = 0

また、セクションに名前を付けることもできます。名前を付けた場合は、閉じるときにも名前を指定する必要があります。

section hoge
  variable (a : Type)

  #check a
end hoge

セクションは入れ子にすることもできます。

section parent
  variable (a : Type)

  section child
    variable (b : Type)

    -- 親セクションで定義された引数は子セクション内でも有効
    #check a
  end child

  -- child セクションの外なので無効
  #check_failure b
end parent

-- parent セクションの外なので無効
#check_failure a

Lean by Example

section