Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

protected のコードの修正 #739

Merged
merged 1 commit into from
Sep 1, 2024
Merged

protected のコードの修正 #739

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 14 additions & 3 deletions Examples/Command/Declarative/Protected.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,17 @@ end Foo

/- `Foo.baz` を `protected` として宣言しておけば、他の名前空間に影響を及ぼさなくなります。-/

protected def Foo.baz := "hello"

def baz := "world"

namespace Foo

-- 単に baz と書いたらルートの baz が参照される
#guard baz = "world"

end Foo

/- ## protected def 以外の用法

`def` コマンドに対してだけでなく、[`indudctive`](./Inductive.md) コマンドで生成されるコンストラクタに対しても使用可能です。-/
Expand Down Expand Up @@ -81,14 +92,14 @@ structure Sample where
protected mk ::

bar : Nat
protected baz : String
protected hoge : String

open Sample

-- 名前空間を開いているので bar には短い名前でアクセスできる
#check bar

-- baz には短い名前でアクセスできない
#check_failure baz
-- hoge には短い名前でアクセスできない
#check_failure hoge

end --#
Loading