Skip to content

Commit

Permalink
chore: move docstrings for open, variable, universe, export from elab…
Browse files Browse the repository at this point in the history 
…orator to parser (#3891)

During the documentation sprint we discussed that user-visible
documentation for syntax should generally go on the parser instead of
the elaborator.
  • Loading branch information
@TwoFX
TwoFX authored Apr 17, 2024
1 parent cefba8a commit d3e0049
Show file tree
Hide file tree
Showing 2 changed files with 291 additions and 291 deletions.
290 changes: 0 additions & 290 deletions src/Lean/Elab/BuiltinCommand.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -119,64 +119,6 @@ private partial def elabChoiceAux (cmds : Array Syntax) (i : Nat) : CommandElabM
@[builtin_command_elab choice] def elabChoice : CommandElab := fun stx =>
elabChoiceAux stx.getArgs 0

/-- Declares one or more universe variables.
`universe u v`
`Prop`, `Type`, `Type u` and `Sort u` are types that classify other types, also known as
*universes*. In `Type u` and `Sort u`, the variable `u` stands for the universe's *level*, and a
universe at level `u` can only classify universes that are at levels lower than `u`. For more
details on type universes, please refer to [the relevant chapter of Theorem Proving in Lean][tpil
universes].
Just as type arguments allow polymorphic definitions to be used at many different types, universe
parameters, represented by universe variables, allow a definition to be used at any required level.
While Lean mostly handles universe levels automatically, declaring them explicitly can provide more
control when writing signatures. The `universe` keyword allows the declared universe variables to be
used in a collection of definitions, and Lean will ensure that these definitions use them
consistently.
[tpil universes]: https://lean-lang.org/theorem_proving_in_lean4/dependent_type_theory.html#types-as-objects
(Type universes on Theorem Proving in Lean)
```lean
/- Explicit type-universe parameter. -/
def id₁.{u} (α : Type u) (a : α) := a
/- Implicit type-universe parameter, equivalent to `id₁`.
Requires option `autoImplicit true`, which is the default. -/
def id₂ (α : Type u) (a : α) := a
/- Explicit standalone universe variable declaration, equivalent to `id₁` and `id₂`. -/
universe u
def id₃ (α : Type u) (a : α) := a
```
On a more technical note, using a universe variable only in the right-hand side of a definition
causes an error if the universe has not been declared previously.
```lean
def L₁.{u} := List (Type u)
-- def L₂ := List (Type u) -- error: `unknown universe level 'u'`
universe u
def L₃ := List (Type u)
```
## Examples
```lean
universe u v w
structure Pair (α : Type u) (β : Type v) : Type (max u v) where
a : α
b : β
#check Pair.{v, w}
-- Pair : Type v → Type w → Type (max v w)
```
-/
@[builtin_command_elab «universe»] def elabUniverse : CommandElab := fun n => do
n[1].forArgsM addUnivLevel

Expand All @@ -185,30 +127,6 @@ structure Pair (α : Type u) (β : Type v) : Type (max u v) where
| Except.ok env => setEnv env
| Except.error ex => throwError (ex.toMessageData (← getOptions))

/-- Adds names from other namespaces to the current namespace.
The command `export Some.Namespace (name₁ name₂)` makes `name₁` and `name₂`:
- visible in the current namespace without prefix `Some.Namespace`, like `open`, and
- visible from outside the current namespace `N` as `N.name₁` and `N.name₂`.
## Examples
```lean
namespace Morning.Sky
def star := "venus"
end Morning.Sky
namespace Evening.Sky
export Morning.Sky (star)
-- `star` is now in scope
#check star
end Evening.Sky
-- `star` is visible in `Evening.Sky`
#check Evening.Sky.star
```
-/
@[builtin_command_elab «export»] def elabExport : CommandElab := fun stx => do
let `(export $ns ($ids*)) := stx | throwUnsupportedSyntax
let nss ← resolveNamespace ns
Expand All @@ -223,118 +141,6 @@ end Evening.Sky
aliases := aliases.push (currNamespace ++ id, declName)
modify fun s => { s with env := aliases.foldl (init := s.env) fun env p => addAlias env p.1 p.2 }

/-- Makes names from other namespaces visible without writing the namespace prefix.
Names that are made available with `open` are visible within the current `section` or `namespace`
block. This makes referring to (type) definitions and theorems easier, but note that it can also
make [scoped instances], notations, and attributes from a different namespace available.
The `open` command can be used in a few different ways:
* `open Some.Namespace.Path1 Some.Namespace.Path2` makes all non-protected names in
`Some.Namespace.Path1` and `Some.Namespace.Path2` available without the prefix, so that
`Some.Namespace.Path1.x` and `Some.Namespace.Path2.y` can be referred to by writing only `x` and
`y`.
* `open Some.Namespace.Path hiding def1 def2` opens all non-protected names in `Some.Namespace.Path`
except `def1` and `def2`.
* `open Some.Namespace.Path (def1 def2)` only makes `Some.Namespace.Path.def1` and
`Some.Namespace.Path.def2` available without the full prefix, so `Some.Namespace.Path.def3` would
be unaffected.
This works even if `def1` and `def2` are `protected`.
* `open Some.Namespace.Path renaming def1 → def1', def2 → def2'` same as `open Some.Namespace.Path
(def1 def2)` but `def1`/`def2`'s names are changed to `def1'`/`def2'`.
This works even if `def1` and `def2` are `protected`.
* `open scoped Some.Namespace.Path1 Some.Namespace.Path2` **only** opens [scoped instances],
notations, and attributes from `Namespace1` and `Namespace2`; it does **not** make any other name
available.
* `open <any of the open shapes above> in` makes the names `open`-ed visible only in the next
command or expression.
[scoped instance]: https://lean-lang.org/theorem_proving_in_lean4/type_classes.html#scoped-instances
(Scoped instances in Theorem Proving in Lean)
## Examples
```lean
/-- SKI combinators https://en.wikipedia.org/wiki/SKI_combinator_calculus -/
namespace Combinator.Calculus
def I (a : α) : α := a
def K (a : α) : β → α := fun _ => a
def S (x : α → β → γ) (y : α → β) (z : α) : γ := x z (y z)
end Combinator.Calculus
section
-- open everything under `Combinator.Calculus`, *i.e.* `I`, `K` and `S`,
-- until the section ends
open Combinator.Calculus
theorem SKx_eq_K : S K x = I := rfl
end
-- open everything under `Combinator.Calculus` only for the next command (the next `theorem`, here)
open Combinator.Calculus in
theorem SKx_eq_K' : S K x = I := rfl
section
-- open only `S` and `K` under `Combinator.Calculus`
open Combinator.Calculus (S K)
theorem SKxy_eq_y : S K x y = y := rfl
-- `I` is not in scope, we have to use its full path
theorem SKxy_eq_Iy : S K x y = Combinator.Calculus.I y := rfl
end
section
open Combinator.Calculus
renaming
I → identity,
K → konstant
#check identity
#check konstant
end
section
open Combinator.Calculus
hiding S
#check I
#check K
end
section
namespace Demo
inductive MyType
| val
namespace N1
scoped infix:68 " ≋ " => BEq.beq
scoped instance : BEq MyType where
beq _ _ := true
def Alias := MyType
end N1
end Demo
-- bring `≋` and the instance in scope, but not `Alias`
open scoped Demo.N1
#check Demo.MyType.val == Demo.MyType.val
#check Demo.MyType.val ≋ Demo.MyType.val
-- #check Alias -- unknown identifier 'Alias'
end
```
-/
@[builtin_command_elab «open»] def elabOpen : CommandElab
| `(open $decl:openDecl) => do
let openDecls ← elabOpenDecl decl
Expand Down Expand Up @@ -420,102 +226,6 @@ private def replaceBinderAnnotation (binder : TSyntax ``Parser.Term.bracketedBin
else
return #[binder]

/-- Declares one or more typed variables, or modifies whether already-declared variables are
implicit.
Introduces variables that can be used in definitions within the same `namespace` or `section` block.
When a definition mentions a variable, Lean will add it as an argument of the definition. The
`variable` command is also able to add typeclass parameters. This is useful in particular when
writing many definitions that have parameters in common (see below for an example).
Variable declarations have the same flexibility as regular function paramaters. In particular they
can be [explicit, implicit][binder docs], or [instance implicit][tpil classes] (in which case they
can be anonymous). This can be changed, for instance one can turn explicit variable `x` into an
implicit one with `variable {x}`. Note that currently, you should avoid changing how variables are
bound and declare new variables at the same time; see [issue 2789] for more on this topic.
See [*Variables and Sections* from Theorem Proving in Lean][tpil vars] for a more detailed
discussion.
[tpil vars]: https://lean-lang.org/theorem_proving_in_lean4/dependent_type_theory.html#variables-and-sections
(Variables and Sections on Theorem Proving in Lean)
[tpil classes]: https://lean-lang.org/theorem_proving_in_lean4/type_classes.html
(Type classes on Theorem Proving in Lean)
[binder docs]: https://leanprover-community.github.io/mathlib4_docs/Lean/Expr.html#Lean.BinderInfo
(Documentation for the BinderInfo type)
[issue 2789]: https://github.com/leanprover/lean4/issues/2789
(Issue 2789 on github)
## Examples
```lean
section
variable
{α : Type u} -- implicit
(a : α) -- explicit
[instBEq : BEq α] -- instance implicit, named
[Hashable α] -- instance implicit, anonymous
def isEqual (b : α) : Bool :=
a == b
#check isEqual
-- isEqual.{u} {α : Type u} (a : α) [instBEq : BEq α] (b : α) : Bool
variable
{a} -- `a` is implicit now
def eqComm {b : α} := a == b ↔ b == a
#check eqComm
-- eqComm.{u} {α : Type u} {a : α} [instBEq : BEq α] {b : α} : Prop
end
```
The following shows a typical use of `variable` to factor out definition arguments:
```lean
variable (Src : Type)
structure Logger where
trace : List (Src × String)
#check Logger
-- Logger (Src : Type) : Type
namespace Logger
-- switch `Src : Type` to be implicit until the `end Logger`
variable {Src}
def empty : Logger Src where
trace := []
#check empty
-- Logger.empty {Src : Type} : Logger Src
variable (log : Logger Src)
def len :=
log.trace.length
#check len
-- Logger.len {Src : Type} (log : Logger Src) : Nat
variable (src : Src) [BEq Src]
-- at this point all of `log`, `src`, `Src` and the `BEq` instance can all become arguments
def filterSrc :=
log.trace.filterMap
fun (src', str') => if src' == src then some str' else none
#check filterSrc
-- Logger.filterSrc {Src : Type} (log : Logger Src) (src : Src) [inst✝ : BEq Src] : List String
def lenSrc :=
log.filterSrc src |>.length
#check lenSrc
-- Logger.lenSrc {Src : Type} (log : Logger Src) (src : Src) [inst✝ : BEq Src] : Nat
end Logger
```
-/
@[builtin_command_elab «variable»] def elabVariable : CommandElab
| `(variable $binders*) => do
-- Try to elaborate `binders` for sanity checking
Expand Down
Loading

0 comments on commit d3e0049

Please sign in to comment.