private

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

注意

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

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

-- PrivateLib.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.PrivateLib -- 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

Lean by Example

private