5.1. Identifiers

$x:ident

An identifier term is a reference to a name.The specific lexical syntax of identifiers is described in the section on Lean's concrete syntax. Identifiers also occur in contexts where they bind names, such as Lean.Parser.Term.let : term`let` is used to declare a local definition. Example: ``` let x := 1 let y := x + 1 x + y ``` Since functions are first class citizens in Lean, you can use `let` to declare local functions too. ``` let double := fun x => 2*x double (double 3) ``` For recursive definitions, you should use `let rec`. You can also perform pattern matching using `let`. For example, assume `p` has type `Nat × Nat`, then you can write ``` let (x, y) := p x + y ``` let and Lean.Parser.Term.fun : termfun; however, these binding occurrences are not complete terms in and of them selves. The mapping from identifiers to names is not trivial: at any point in a module, some number of namespaces will be open, there may be section variables, and there may be local bindings. Furthermore, identifiers may contain multiple dot-separated atomic identifiers; the dot both separates namespaces from their contents and variables from fields or functions that use field notation. This creates ambiguity, because an identifier A.B.C.D.e.f could refer to any of the following:

• A name f in the namespace A.B.C.D.e (for instance, a function defined in e's Lean.Parser.Command.declaration : commandwhere block).

• An application of T.f to A.B.C.D.e if A.B.C.D.e has type T

• A projection of field f from a structure named A.B.C.D.e

• A series of field projections B.C.D.e from structure value A, followed by an application of f using field notation

• If namespace Q is opened, it could be a reference to any of the above with a Q prefix, such as a name f in the namespace Q.A.B.C.D.e

This list is not exhaustive. Given an identifier, the elaborator must discover which name or names an identifier refers to, and whether any of the trailing components are fields or functions applied via field notation. This is called resolving the name.

Some declarations in the global environment are lazily created the first time they are referenced. Resolving an identifier in a way that both creates one of these declarations and results in a reference to it is called realizing the name. The rules for resolving and realizing a name are the same, so even though this section refers only to resolving names, it applies to both.

Name resolution is affected by the following:

• Pre-resolved names attached to the identifier

• The macro scopes attached to the identifier

• The local bindings in scope, including auxiliary definitions created as part of the elaboration of Lean.Parser.Term.letrec : termlet rec.

• Aliases created with Lean.Parser.Command.export : commandAdds 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 ``` export in modules transitively imported by the current module

• The current section scope, in particular the current namespace, opened namespaces, and section variables

Any prefix of an identifier can resolve to a set of names. The suffix that was not included in the resolution process is then treated as field projections or field notation. Resolutions of longer prefixes take precedence over resolutions of shorter prefixes; in other words, as few components as of the identifier as possible are treated as field notation. An identifier prefix may refer to any of the following, with earlier items taking precedence over later ones:

1. A locally-bound variable whose name is identical to the identifier prefix, including macro scopes, with closer local bindings taking precedence over outer local bindings.

2. A local auxiliary definition whose name is identical to the identifier prefix

3. A section variable whose name is identical to the identifier prefix

4. A global name that is identical to a prefix of the current namespace appended to the identifier prefix, or for which an alias exists in a prefix of the current namespace, with longer prefixes of the current namespace taking precedence over shorter ones

5. A global name that has been brought into scope via Lean.Parser.Command.open : commandMakes 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 ``` open commands that is identical to the identifier prefix

If an identifier resolves to multiple names, then the elaborator attempts to use all of them. If exactly one of them succeeds, then it is used as the meaning of the identifier. It is an error if more than one succeed or if all fail.

"local"

"inner"

"A.B.C.x"

"A.x"

"longer"

"B.x"

ambiguous, possible interpretations 
  B.x : String
  
  A.x : String

"C.x"

[(), (), ()]

[(), (), ()]