Merge pull request #1342 from lean-ja/Seasawher/issue1335

不要なnamesapceを使用しない

Author: Seasawher

LeanByExample/Attribute/AppUnexpander.lean

@@ -1,7 +1,6 @@
 /- # app_unexpander
 `[app_unexpander]` 属性を付与すると、関数適用 `f a₁ a₂ ... aₙ` の `#check` コマンドおよび infoview での表示のされ方を変更することができます。
 -/
-namespace AppUnexpander --#
 
 /-- 人に挨拶をする関数 -/
 def greet (x : String) := s!"Hello, {x}!"
@@ -69,5 +68,3 @@ def setOf.unexpander : Lean.PrettyPrinter.Unexpander
 /-- info: {n | ∃ m, n = 2 * m} : Set Nat -/
 #guard_msgs in
   #check {n : Nat | ∃ m, n = 2 * m}
-
-end AppUnexpander --#

LeanByExample/Attribute/Csimp.lean

@@ -4,7 +4,6 @@
 `A = B` という形の定理に付与することでコンパイラに `A` の計算を `B` の計算に置き換えさせることができます。非効率な関数を効率的な実装に置き換えるために使用されます。
 -/
 import Lean
-namespace Csimp --#
 
 /-- フィボナッチ数列の非効率な実装 -/
 def fibonacci : Nat → Nat
@@ -27,7 +26,8 @@ elab "#in_second " stx:command : command => do
 
 -- `#eval fibonacci 32` は１秒以上かかる
 /-- error: It took more than one second for the command to run. -/
-#guard_msgs (error) in #in_second #eval fibonacci 32
+#guard_msgs (error) in
+  #in_second #eval fibonacci 32
 
 /-- フィボナッチ数列のより高速な実装 -/
 def fib (n : Nat) : Nat :=
@@ -58,5 +58,3 @@ theorem fib_eq_fibonacci : fibonacci = fib := by
 -- `fibonacci` の計算が１秒以内に終わるようになった
 #in_second #eval fibonacci 32
 #in_second #eval fibonacci 132
-
-end Csimp --#

LeanByExample/Declarative/Attribute.lean

@@ -5,7 +5,6 @@
 
 次の例では、命題に `[simp]` 属性を付与しています。これは `simp` タクティクで利用される命題を増やすことを意味します。
 -/
-namespace Attribute --#
 
 theorem foo {P Q : Prop} : (P → Q) ∧ P ↔ Q ∧ P := by
   constructor <;> intro h
@@ -102,5 +101,3 @@ example (P Q : Prop) : ((P ∨ Q) ∧ ¬ Q) ↔ (P ∧ ¬ Q) := by
   | simp
 
   sorry
-
-end Attribute --#

LeanByExample/Declarative/Axiom.lean

@@ -1,7 +1,6 @@
 /- # axiom
 `axiom` は、公理(axiom)を宣言するためのコマンドです。公理とは、議論の前提のことで、証明を与えることなく正しいと仮定される命題です。
 -/
-namespace Axiom --#
 
 /-- sorryAx を真似て作った公理 -/
 axiom mySorryAx {P : Prop} : P
@@ -10,7 +9,7 @@ axiom mySorryAx {P : Prop} : P
 theorem FLT : ∀ x y z n : Nat, n > 2 → x^n + y^n ≠ z^n := by
   apply mySorryAx
 
-/-- info: 'Axiom.FLT' depends on axioms: [Axiom.mySorryAx] -/
+/-- info: 'FLT' depends on axioms: [mySorryAx] -/
 #guard_msgs in #print axioms FLT
 
 /- ## 組み込みの公理
@@ -30,8 +29,9 @@ theorem ex_prop_ext (a b : Prop) (p : Prop → Prop) (h : a ↔ b) (h₁ : p a)
   rw [←this]
   assumption
 
-/-- info: 'Axiom.ex_prop_ext' depends on axioms: [propext] -/
-#guard_msgs in #print axioms ex_prop_ext
+/-- info: 'ex_prop_ext' depends on axioms: [propext] -/
+#guard_msgs in
+  #print axioms ex_prop_ext
 
 /- ### 商の公理 Quot.sound
 任意の型 `α : Sort u` と `α` 上の2項関係 `r : α → α → Prop` に対して、その商(quotient)を作ることができます。商の概念は、以下に示す複数の定数から構成されます。
@@ -134,7 +134,7 @@ theorem lambda_eq (f : (x : α) → β x) : f = (fun x => f x) := by rfl
 
 -- 依存関数 `f` がラムダ式 `fun x => f x` に等しいことは、定義から従うので
 -- 何の公理も必要としない。
-/-- info: 'Axiom.lambda_eq' does not depend on any axioms -/
+/-- info: 'lambda_eq' does not depend on any axioms -/
 #guard_msgs in
   #print axioms lambda_eq
 
@@ -153,7 +153,7 @@ theorem funApp_eq (f : (x : α) → β x) : funApp (f := f) = f := calc
   _ = f := by rw [lambda_eq f]
 
 -- これも何の公理も必要としない
-/-- info: 'Axiom.funApp_eq' does not depend on any axioms -/
+/-- info: 'funApp_eq' does not depend on any axioms -/
 #guard_msgs in
   #print axioms funApp_eq
 
@@ -199,7 +199,7 @@ theorem my_funext {f g : (x : α) → β x} (h : ∀ x, f x = g x) : f = g := by
     -- 「`g` を適用する関数」と `g` は等しい
     _ = g := by rw [funApp_eq g]
 
-/-- info: 'Axiom.my_funext' depends on axioms: [Quot.sound] -/
+/-- info: 'my_funext' depends on axioms: [Quot.sound] -/
 #guard_msgs in #print axioms my_funext
 
 /- ### 選択原理 Classical.choice { #ClassicalChoice }
@@ -286,7 +286,7 @@ theorem lemma_em (himp : P → Q) (hor : ¬ Q ∨ P) : P ∨ ¬ P := by
     exact h
 
 -- 何の公理も使用していない
-/-- info: 'Axiom.lemma_em' does not depend on any axioms -/
+/-- info: 'lemma_em' does not depend on any axioms -/
 #guard_msgs in #print axioms lemma_em
 
 /- 選択原理を用いると命題 `Q` を構成することができ、関数外延性と命題外延性により、それが所望の性質を持つことを示すことができます。-/
@@ -349,5 +349,3 @@ theorem em (P : Prop) : P ∨ ¬ P := by
 
     -- 残りの１つでは `u ≠ v` が成り立つ。
     simp [hu, hv]
-
-end Axiom --#

LeanByExample/Declarative/Class.lean

@@ -2,7 +2,6 @@
 # class
 `class` は **型クラス(type class)** を定義するためのコマンドです。型クラスを用いると、複数の型に対して定義され、型ごとに異なる実装を持つような関数を定義することができます。例えば「和を取る操作」のような、`Nat` や `Int` や `Rat` など複数の型に対して同じ名前で定義したい関数を作りたいとき、型クラスが適しています。
 -/
-namespace Class --#
 /-- 証明なしのバージョンのモノイド。
 ただしモノイドとは、要素同士を「くっつける」操作ができて、
 くっつけても変わらない要素があるようなもののこと。-/
@@ -197,5 +196,3 @@ export HasCardinal (card)
 
 -- Bool の濃度が計算できた
 #guard card Bool = Ordinal.nat 2
-
-end Class --#

LeanByExample/Declarative/DeclareSyntaxCat.lean

@@ -4,7 +4,6 @@
 
 例として、集合の内包表記 `{x : T | P x}` を定義するコードを示します。
 -/
-namespace DeclareSyntaxCat --#
 
 universe u
 
@@ -61,5 +60,3 @@ macro_rules
 #check
   let Even := { x : Nat | x % 2 = 0 }
   { x ∈ Even | x > 0 }
-
-end DeclareSyntaxCat --#

LeanByExample/Declarative/Infix.lean

@@ -3,34 +3,31 @@
 `infix` は、中置記法を定義するコマンドです。
 -/
 import Lean --#
-namespace Infix --#
 
 -- 中置記法を定義。中身はただの掛け算
--- 特定の名前空間でだけ有効にするために `scoped` を付けている
-scoped infix:60 " ⋄ " => Nat.mul
+infix:60 " ⋄ " => Nat.mul
 
 #guard 2 ⋄ 3 = 6
 
 /- `:` の後に付けている数字は **パース優先順位(parsing precedence)** で、高いほど結合するタイミングが早くなります。等号 `=` のパース優先順位は 50 であることを覚えておくと良いかもしれません。-/
 
 -- 等号より微妙にパース優先順位が高い
-scoped infix:51 " strong " => Nat.add
+infix:51 " strong " => Nat.add
 
 -- きちんと 1 + (2 strong 3) = 6 と解釈される。
 -- これは、 等号のパース優先順位が 51 未満であることを意味する
 #check 1 + 2 strong 3 = 6
 
 -- パース優先順位を 50 より低くすると等号より低くなる
 -- したがってエラーになる
-scoped infix:49 " weak " => Nat.add
+infix:49 " weak " => Nat.add
 
 #guard_msgs (drop warning) in --#
 #check_failure 1 + 2 weak 3 = 6
 
 /- `infix` で定義される記法は左結合でも右結合でもなく、必ず括弧が必要です。-/
-section
 
-open Lean Parser
+open Lean Parser in
 
 /-- `s : String` をパースして `Syntax` の項を得る。`cat` は構文カテゴリ。-/
 def parse (cat : Name) (s : String) : MetaM Syntax := do
@@ -43,7 +40,6 @@ def parse (cat : Name) (s : String) : MetaM Syntax := do
 -- 括弧を付ければOK
 #eval parse `term "1 ⋄ (2 ⋄ 3)"
 
-end
 /- ## 舞台裏
 
 `infix` は [`notation`](./Notation.md) コマンドに展開されるマクロとして実装されています。-/
@@ -68,5 +64,3 @@ elab "#expand " t:macro_stx : command => do
 /-- info: notation:50 lhs✝:51 " LXOR " rhs✝:51 => lxor lhs✝ rhs✝ -/
 #guard_msgs in
   #expand infix:50 " LXOR " => lxor
-
-end Infix --#

LeanByExample/Declarative/Instance.lean

@@ -2,7 +2,6 @@
 # instance
 `instance` は、型クラスのインスタンスを定義するためのコマンドです。
 -/
-namespace Instance --#
 
 /-- 平面 -/
 structure Point (α : Type) where
@@ -94,5 +93,3 @@ attribute [-instance] instListAdd
 -- リスト同士を足すことができなくなった
 #guard_msgs (drop warning) in --#
 #check_failure [1] + [2]
-
-end Instance --#

LeanByExample/Declarative/Postfix.lean

@@ -3,16 +3,14 @@
 `postfix` は、後置記法を定義するコマンドです。
 -/
 import Lean --#
-namespace Postfix --#
 
 /-- 階乗 -/
 def factorial : Nat → Nat
   | 0 => 1
   | n + 1 => (n + 1) * factorial n
 
 -- 後置記法を定義する
--- scoped を付けたのは、この後置記法をこの名前空間内でのみ有効にするため
-scoped postfix:200 "!" => factorial
+postfix:200 "!" => factorial
 
 -- 定義した記法が使える
 #guard 5! = 120
@@ -39,5 +37,3 @@ elab "#expand " t:macro_stx : command => do
 /-- info: notation:200 arg✝:200 "!" => factorial arg✝ -/
 #guard_msgs in
   #expand postfix:200 "!" => factorial
-
-end Postfix --#

LeanByExample/Declarative/Prefix.lean

@@ -3,12 +3,10 @@
 `prefix` は、前置記法を定義するためのコマンドです。
 -/
 import Lean --#
-namespace Prefix --#
 
 -- 前置記法を定義
 -- 中身は Nat.succ
--- scoped を付けているのは、この記法をこの名前空間でのみ有効にするため
-scoped prefix:90 "⋄" => Nat.succ
+prefix:90 "⋄" => Nat.succ
 
 -- 上で定義した記法が使える
 #guard ⋄3 = 4
@@ -35,5 +33,3 @@ elab "#expand " t:macro_stx : command => do
 /-- info: notation:90 "⋄" arg✝:90 => Nat.succ arg✝ -/
 #guard_msgs in
   #expand prefix:90 "⋄" => Nat.succ
-
-end Prefix --#

LeanByExample/Declarative/Structure.lean

@@ -2,7 +2,6 @@
 # structure
 `structure` は構造体を定義するためのコマンドです。構造体とは、複数のデータをまとめて一つの型として扱えるようにしたものです。
 -/
-namespace Structure --#
 
 /-- 2次元空間の点 -/
 structure Point (α : Type) : Type where
@@ -30,6 +29,7 @@ example : Point.x origin = 0 := by rfl
 #check (Point.mk : {α : Type} → α → α → Point α)
 
 /- コンストラクタに `mk` 以外の名前を使いたい場合、`::` を使って次のようにします。-/
+namespace Hidden --#
 
 structure Prod (α : Type) (β : Type) where
   gen ::
@@ -39,6 +39,7 @@ structure Prod (α : Type) (β : Type) where
 -- コンストラクタの名前が gen になっている
 #check Prod.gen
 
+end Hidden --#
 /- ## フィールド記法 { #FieldNotation }
 構造体 `S` の項 `s : S` に `x` というフィールドがあるとき、`S.x s` の代わりに `s.x` と書くことができます。これにより、`s : S` におけるフィールド `x` の値を取得することができます。この関数適用を省略して「あたかもフィールドのように」値にアクセスする記法のことを **フィールド記法(field notation)** といいます。
 
@@ -178,5 +179,3 @@ warning: invalid {...} notation, structure type expected
 -/
 #guard_msgs in
   #check_failure ({ x := 1, y := 2 } : Point' Int)
-
-end Structure --#

LeanByExample/Declarative/Theorem.lean

@@ -2,7 +2,6 @@
 # theorem
 `theorem` は名前付きで命題を証明するためのコマンドです。より正確には、`theorem` は証明項を定義するためのコマンドだといえます。
 -/
-namespace Theorem --#
 
 /-- 自然数に右から0を足しても変わらない -/
 theorem add_zero {n : Nat} : n + 0 = n := by simp
@@ -16,13 +15,11 @@ theorem add_zero {n : Nat} : n + 0 = n := by simp
 def add_zero' {n : Nat} : n + 0 = n := by simp
 
 /--
-error: type of theorem 'Theorem.frac' is not a proposition
+error: type of theorem 'frac' is not a proposition
   Nat → Nat
 -/
 #guard_msgs (whitespace := lax) in --#
 theorem frac (n : Nat) : Nat :=
   match n with
   | 0 => 1
   | n + 1 => (n + 1) * frac n
-
-end Theorem --#

LeanByExample/Diagnostic/Guard.lean

@@ -3,8 +3,6 @@
 -/
 import Batteries.Data.List.Lemmas -- リストに対して `⊆` が使えるようにする
 
-namespace guard --#
-
 -- 階乗関数
 def fac : Nat → Nat
 | 0 => 1
@@ -32,7 +30,7 @@ but is expected to have type
 error: cannot evaluate code because 'sorryAx' uses 'sorry' and/or contains errors
 -/
 #guard_msgs (whitespace := lax) in
-#guard ((α : Type) → ∀ (l : List α), [] ⊆ l : Prop)
+  #guard ((α : Type) → ∀ (l : List α), [] ⊆ l : Prop)
 
 /- しかし、 `1 + 1 = 2` 等も `#check` で確かめてみると型は `Prop` です。にも関わらず `#guard` に渡してもエラーになりません。これは不思議に思えますが、理由は `1 + 1 = 2` が [`Decidable`](../TypeClass/Decidable.md) 型クラスのインスタンスであり、決定可能だからです。-/
 
@@ -54,6 +52,5 @@ error: cannot evaluate code because 'sorryAx' uses 'sorry' and/or contains error
 
 -- Bool 型になっている
 /-- info: decide (1 + 1 = 2) : Bool -/
-#guard_msgs in #check decide (1 + 1 = 2)
-
-end guard --#
+#guard_msgs in
+  #check decide (1 + 1 = 2)

LeanByExample/Diagnostic/Reduce.lean

@@ -1,7 +1,6 @@
 /- # \#reduce
 `#reduce` は、与えられた式をこれ以上簡約できなくなるまで簡約します。
 -/
-namespace Reduce --#
 
 /-- info: 4 -/
 #guard_msgs in #reduce 1 + 3
@@ -20,5 +19,3 @@ def addOne (x : Nat) := x + 1
 -- 合成が計算できる
 /-- info: fun x => x.succ.succ -/
 #guard_msgs in #reduce addOne ∘ addOne
-
-end Reduce --#

LeanByExample/Diagnostic/Time.lean

@@ -2,7 +2,6 @@
 `#time` は、コマンドの実行時間を計測するためのコマンドです。ミリ秒単位で結果を出してくれます。
 -/
 import Lean
-namespace Time --#
 
 -- フィボナッチ数列の遅い実装
 -- `n` に関して指数関数的な時間がかかる
@@ -78,5 +77,3 @@ elab "#in_second " stx:command : command => do
 /-- error: It took more than one second for the command to run. -/
 #guard_msgs (error) in
   #in_second #eval fibonacci 32
-
-end Time --#

LeanByExample/Modifier/PrivateLib.lean

@@ -6,9 +6,9 @@ structure Point where
 
 namespace Point
 
-protected def sub (p q : Point) : Point :=
-    { x := p.x - q.x, y := p.y - q.y }
+  protected def sub (p q : Point) : Point :=
+      { x := p.x - q.x, y := p.y - q.y }
 
-private def private_sub := Point.sub
+  private def private_sub := Point.sub
 
 end Point