Skip to content

Commit 4dc783b

Browse files
committed
ビルドが通らない問題を修正
1 parent 8ff34a0 commit 4dc783b

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

LeanByExample/Reference/Declarative/Private.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
44
不安定なAPIなど、外部に公開したくないものに対して使うのが主な用途です。
55
-/
6-
import Examples.Declarative.Protected -- protected のページをインポート
6+
import LeanByExample.Reference.Declarative.Protected -- protected のページをインポート
77
import Lean
88
namespace Private --#
99

0 commit comments

Comments
 (0)