private

private は、その定義があるファイルの中でだけ参照可能になるようにする修飾子です。他のファイルからはアクセス不能になります。不安定なAPIなど、外部に公開したくないものに対して使うのが主な用途です。

注意

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

たとえば、以下のように書かれているファイル Private/Lib.lean があったとしましょう。

structure Point where
  x : Nat
  y : Nat

namespace Point

  protected def sub (p q : Point) : Point :=
      { x := p.x - q.x, y := p.y - q.y }

  private def private_sub := Point.sub

end Point

このとき、モジュール PrivateLib を読み込んでいるファイルからは、protected で修飾された名前はアクセス可能ですが、private で修飾された名前はアクセスできません。

import LeanByExample.Modifier.Private.Lib -- private が使用されているモジュールをインポート

-- private を使わずに定義した内容にはアクセスできる
#check Point.sub

-- private とマークした定義にはアクセスできない
#check_failure Point.private_sub

なお private コマンドで定義した名前は、同じファイル内であればそのセクションや名前空間を出ても普通にアクセスすることができます。特に、private は protected の効果を持ちません。

namespace Hoge
  section
    -- private とマークした定義
    private def addOne (n : Nat) : Nat := n + 1

  end
end Hoge

open Hoge

-- 外からでもアクセスできる
#check addOne

補足: privateで隠された定義に一時的にアクセスする

private で隠された定義にアクセスする方法はあります。手軽なのは、open private コマンドを使う方法です。

import LeanByExample.Modifier.Private.Lib
import Batteries.Tactic.OpenPrivate

-- 最初はアクセスできない
#check_failure Point.private_sub

-- `open private` コマンドを使用する
open private Point.private_sub from LeanByExample.Modifier.Private.Lib

-- アクセスできるようになった
#check Point.private_sub