翻译-Lean Language Reference-06-命名空间和区段

def color := "yellow" -- _root_.color
namespace Forest
def color := "green"  -- _root_.Forest.color
def statement := s!"Lemons are {color}"
end Forest
#eval Forest.statement
-- "Lemons are green"

namespace Forest
def nextStatement :=
  s!"Ripe lemons are {_root_.color}, not {color}"
end Forest
#eval Forest.nextStatement
-- "Ripe lemons are yellow, not green"

inductive HotDrink where
  | coffee
  | tea
  | cocoa

#check HotDrink.tea
-- HotDrink.tea : HotDrink

#check tea
-- Unknown identifier `tea`

section
open HotDrink
#check tea
-- HotDrink.tea : HotDrink
end

def HotDrink.ofString? (s : String) := match s with
  | "coffee" => some coffee -- 这里能自动推断出是 HotDrink.coffee
  | "tea"    => some tea    -- 这里能自动推断出是 HotDrink.tea
  | "cocoa"  => some cocoa  -- 这里能自动推断出是 HotDrink.cocoa
  | _ => none

inductive ColdDrink where
  | water
  | juice

namespace HotDrink

def toString : HotDrink → String
  | coffee => "coffee"
  | tea => "tea"
  | cocoa => "cocoa"

def _root_.ColdDrink.toString : ColdDrink → String
  | .water => "water"
  | .juice => "juice"

end HotDrink

namespace A -- _root_.A
def a1 := "A.a1"
namespace B -- _root_.A.B
def a2 := "A.B.a2"
namespace C -- _root_.A.B.C
def a3 := "A.B.C.a3"
end C
end B
end A
namespace B -- _root_.B
def a4 := "B.a4"
namespace C -- _root_.B.C
def a5 := "B.C.a5"
end C
end B
namespace C -- _root_.C
def a6 := "C.a6"
namespace B -- _root_.C.B
def a7 := "C.B.a7"
end B
end C

section
open A B C
example := [a1, a2, a3, a4, a5, a6, a7]
-- Unknown identifier `a7`
end

section
open A.B C
example := [a1, a2, a3, a4, a5, a6]
end
-- Unknown identifier `a1`
-- Unknown identifier `a4`
-- Unknown identifier `a5`

namespace NS
scoped notation "{!{" e "}!}" => (e, e)
def three := 3
end NS

def x := {!{ "pear" }!}
-- <example>:1:21-1:22: unexpected token '!'; expected '}'

open scoped NS
def x := {!{ "pear" }!}

def y := three
-- Unknown identifier `three`

namespace Veg
inductive Leafy where
  | spinach
  | cabbage
export Leafy (spinach)
end Veg
export Veg.Leafy (cabbage)

def Greetings.english := "Hello"

#eval english
-- Unknown identifier `english`

section Greetings

#eval english
-- Unknown identifier `english`

open Greetings
#eval english
-- "Hello"

end
-- Missing name after `end`: Expected the current scope name `Greetings`
-- 
-- Hint: To end the current scope `Greetings`, specify its name:
--   end ̲G̲r̲e̲e̲t̲i̲n̲g̲s̲
end Greetings

#eval english
-- Unknown identifier `english`

namespace A.B
namespace C
end B.C

section
namespace D.E

end A.D.E
-- Invalid name after `end`: Expected `D.E`, but found `A.D.E`

end D.E
end
end A

def Dessert.cupcake := "delicious"

open Dessert in
#eval cupcake

#eval cupcake
-- Unknown identifier `cupcake`

section
set_option autoImplicit false
universe u
variable {α : Type u} (xs : List α) [Zero α] [Add α]

def addAll (lst : List β) : β :=
  lst.foldr (init := 0) (· + ·)
-- Unknown identifier `β`
-- 
-- Note: It is not possible to treat `β` as an implicitly bound variable here 
-- because the `autoImplicit` option is set to `false`.

def addAll :=
  xs.foldr (init := 0) (· + ·)

variable (length : Nat)

def copies (x : α) : List α :=
  match length with
  | 0 => []
  | length' + 1 => x :: copies length' x

-- Function expected at
--   copies length'
-- but this term has type
--   List Nat
-- Note: Expected a function because 
-- this term is being applied to the argument
--   x

def copies (length : Nat) (x : α) : List α :=
  match length with
  | 0 => []
  | length' + 1 => x :: copies length' x

section
variable {p : Nat → Prop}
variable (pZero : p 0) (pStep : ∀ n, p n → p (n + 1))
variable (pFifteen : p 15)

theorem p_all : ∀ n, p n := by
  intro n
  induction n
-- unsolved goals

include pZero pStep pFifteen

theorem p_all : ∀ n, p n := by
  intro n
  induction n <;> simp [*]
-- automatically included section variable(s) unused in theorem `p_all`:
--   pFifteen
-- consider restructuring your `variable` declarations so that 
-- the variables are not in scope or explicitly omit them:
--   omit pFifteen in theorem ...
-- Note: This linter can be disabled with 
-- `set_option linter.unusedSectionVars false`

include pZero pStep pFifteen

omit pFifteen in
theorem p_all : ∀ n, p n := by
  intro n
  induction n <;> simp [*]
end