Documentation

Lean.Elab.BuiltinCommand

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              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.

              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.

              /- 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.

              def L₁.{u} := List (Type u)
              
              -- def L₂ := List (Type u) -- error: `unknown universe level 'u'`
              
              universe u
              def L₃ := List (Type u)
              

              Examples #

              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)
              
              Equations
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  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 #

                  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
                  
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    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.

                    Examples #

                    /-- 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
                    
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For

                      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, or instance implicit (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 for a more detailed discussion.

                      Examples #

                      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:

                      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
                      
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  @[implemented_by Lean.Elab.Command.elabEvalUnsafe]
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          Equations
                                          Instances For