Documentation

Lean.LocalContext

  • default: Lean.LocalDeclKind

    Participates fully in type class search, tactics, and is shown even if inaccessible.

    For example: the x in fun x => _ has the default kind.

  • implDetail: Lean.LocalDeclKind

    Invisible to type class search or tactics, and hidden in the goal display.

    This kind is used for temporary variables in macros. For example: return (← foo) + bar expands to foo >>= fun __tmp => pure (__tmp + bar), where __tmp has the implDetail kind.

  • auxDecl: Lean.LocalDeclKind

    Auxiliary local declaration for recursive calls. The behavior is similar to implDetail.

    For example: def foo (n : Nat) : Nat := _ adds the local declaration foo : NatNat to allow recursive calls. This declaration has the auxDecl kind.

Whether a local declaration should be found by type class search, tactics, etc. and shown in the goal display.

Instances For
    inductive Lean.LocalDecl :

    A declaration for a LocalContext. This is used to register which free variables are in scope. Each declaration comes with

    • index the position of the decl in the local context
    • fvarId the unique id of the free variables
    • userName the pretty-printable name of the variable
    • type the type. A cdecl is a local variable, a ldecl is a let-bound free variable with a value : Expr.
    Instances For
      Equations
      @[export lean_mk_local_decl]
      def Lean.mkLocalDeclEx (index : Nat) (fvarId : Lean.FVarId) (userName : Lake.Name) (type : Lean.Expr) (bi : Lean.BinderInfo) :
      Equations
      Instances For
        @[export lean_mk_let_decl]
        def Lean.mkLetDeclEx (index : Nat) (fvarId : Lean.FVarId) (userName : Lake.Name) (type : Lean.Expr) (val : Lean.Expr) :
        Equations
        Instances For
          @[export lean_local_decl_binder_info]
          Equations
          Instances For
            Equations
            Instances For
              Equations
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  Equations
                  Instances For
                    Equations
                    Instances For
                      Equations
                      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

                              Is the local declaration an implementation-detail hypothesis (including auxiliary declarations)?

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

                                              A LocalContext is an ordered set of local variable declarations. It is used to store the free variables (also known as local constants) that are in scope.

                                              When inspecting a goal or expected type in the infoview, the local context is all of the variables above the symbol.

                                              Instances For
                                                Equations
                                                @[export lean_mk_empty_local_ctx]
                                                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
                                                    @[export lean_local_ctx_is_empty]
                                                    Equations
                                                    Instances For

                                                      Low level API for creating local declarations. It is used to implement actions in the monads Elab and Tactic. It should not be used directly since the argument (fvarId : FVarId) is assumed to be unique. You can create a unique fvarId with mkFreshFVarId.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        def Lean.LocalContext.mkLetDecl (lctx : Lean.LocalContext) (fvarId : Lean.FVarId) (userName : Lake.Name) (type : Lean.Expr) (value : Lean.Expr) (nonDep : optParam Bool false) (kind : optParam Lean.LocalDeclKind default) :

                                                        Low level API for let declarations. Do not use directly.

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

                                                          Low level API for adding a local declaration. Do not use directly.

                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            @[export lean_local_ctx_find]
                                                            Equations
                                                            Instances For
                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For

                                                                Gets the declaration for expression e in the local context. If e is not a free variable or not present then panics.

                                                                Equations
                                                                Instances For
                                                                  Equations
                                                                  Instances For

                                                                    Returns true when the lctx contains the free variable e. Panics if e is not an fvar.

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

                                                                        Return all of the free variables in the given context.

                                                                        Equations
                                                                        Instances For
                                                                          @[export lean_local_ctx_erase]
                                                                          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
                                                                                      @[inline]

                                                                                      Low-level function for updating the local context. Assumptions about f, the resulting nested expressions must be definitionally equal to their original values, the index nor fvarId are modified.

                                                                                      Equations
                                                                                      • One or more equations did not get rendered due to their size.
                                                                                      Instances For
                                                                                        @[export lean_local_ctx_num_indices]
                                                                                        Equations
                                                                                        Instances For
                                                                                          @[specialize #[]]
                                                                                          def Lean.LocalContext.foldlM {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (lctx : Lean.LocalContext) (f : βLean.LocalDeclm β) (init : β) (start : optParam Nat 0) :
                                                                                          m β
                                                                                          Equations
                                                                                          • One or more equations did not get rendered due to their size.
                                                                                          Instances For
                                                                                            @[specialize #[]]
                                                                                            def Lean.LocalContext.foldrM {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (lctx : Lean.LocalContext) (f : Lean.LocalDeclβm β) (init : β) :
                                                                                            m β
                                                                                            Equations
                                                                                            Instances For
                                                                                              @[specialize #[]]
                                                                                              def Lean.LocalContext.forM {m : Type u_1 → Type u_2} [Monad m] (lctx : Lean.LocalContext) (f : Lean.LocalDeclm PUnit) :
                                                                                              Equations
                                                                                              Instances For
                                                                                                @[specialize #[]]
                                                                                                def Lean.LocalContext.findDeclM? {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (lctx : Lean.LocalContext) (f : Lean.LocalDeclm (Option β)) :
                                                                                                m (Option β)
                                                                                                Equations
                                                                                                Instances For
                                                                                                  @[specialize #[]]
                                                                                                  def Lean.LocalContext.findDeclRevM? {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (lctx : Lean.LocalContext) (f : Lean.LocalDeclm (Option β)) :
                                                                                                  m (Option β)
                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    Equations
                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                    @[inline]
                                                                                                    def Lean.LocalContext.foldl {β : Type u_1} (lctx : Lean.LocalContext) (f : βLean.LocalDeclβ) (init : β) (start : optParam Nat 0) :
                                                                                                    β
                                                                                                    Equations
                                                                                                    Instances For
                                                                                                      @[inline]
                                                                                                      def Lean.LocalContext.foldr {β : Type u_1} (lctx : Lean.LocalContext) (f : Lean.LocalDeclββ) (init : β) :
                                                                                                      β
                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        Equations
                                                                                                        Instances For
                                                                                                          @[inline]
                                                                                                          Equations
                                                                                                          Instances For

                                                                                                            Given lctx₁ - exceptFVars of the form (x_1 : A_1) ... (x_n : A_n), then return true iff there is a local context B_1* (x_1 : A_1) ... B_n* (x_n : A_n) which is a prefix of lctx₂ where B_i's are (possibly empty) sequences of local declarations.

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

                                                                                                                Creates the expression fun x₁ .. xₙ => b for free variables xs = #[x₁, .., xₙ], suitably abstracting b and the types for each of the xᵢ.

                                                                                                                Equations
                                                                                                                Instances For

                                                                                                                  Creates the expression (x₁:α₁) → .. → (xₙ:αₙ) → b for free variables xs = #[x₁, .., xₙ], suitably abstracting b and the types for each of the xᵢ, αᵢ.

                                                                                                                  Equations
                                                                                                                  Instances For
                                                                                                                    @[inline]
                                                                                                                    def Lean.LocalContext.anyM {m : TypeType u_1} [Monad m] (lctx : Lean.LocalContext) (p : Lean.LocalDeclm Bool) :
                                                                                                                    Equations
                                                                                                                    Instances For
                                                                                                                      @[inline]
                                                                                                                      def Lean.LocalContext.allM {m : TypeType u_1} [Monad m] (lctx : Lean.LocalContext) (p : Lean.LocalDeclm Bool) :
                                                                                                                      Equations
                                                                                                                      Instances For
                                                                                                                        @[inline]

                                                                                                                        Return true if lctx contains a local declaration satisfying p.

                                                                                                                        Equations
                                                                                                                        Instances For
                                                                                                                          @[inline]

                                                                                                                          Return true if all declarations in lctx satisfy p.

                                                                                                                          Equations
                                                                                                                          Instances For

                                                                                                                            If option pp.sanitizeNames is set to true, add tombstone to shadowed local declaration names and ones contains macroscopes.

                                                                                                                            Equations
                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                            Instances For
                                                                                                                              class Lean.MonadLCtx (m : TypeType) :

                                                                                                                              Class used to denote that m has a local context.

                                                                                                                              Instances
                                                                                                                                instance Lean.instMonadLCtx {m : TypeType} {n : TypeType} [MonadLift m n] [Lean.MonadLCtx m] :
                                                                                                                                Equations
                                                                                                                                • Lean.instMonadLCtx = { getLCtx := liftM Lean.getLCtx }
                                                                                                                                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