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

chore: move docstrings for open, variable, universe, export from elaborator to parser #3891

Merged
merged 1 commit into from
Apr 17, 2024
Merged

chore: move docstrings for open, variable, universe, export from elaborator to parser #3891

Show file tree
Hide file tree
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
290 changes: 0 additions & 290 deletions src/Lean/Elab/BuiltinCommand.lean
View file
Open in desktop
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
Loading