# Documentation

Lean.LocalContext

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

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

default: 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.

implDetail: 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 : Nat → Nat to allow recursive calls. This declaration has the auxDecl kind.

auxDecl: Lean.LocalDeclKind

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

Instances For
Equations
Equations
inductive Lean.LocalDecl :
• cdecl:
• ldecl:

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 : Lean.Name) (type : Lean.Expr) (bi : Lean.BinderInfo) :
Equations
@[export lean_mk_let_decl]
def Lean.mkLetDeclEx (index : Nat) (fvarId : Lean.FVarId) (userName : Lean.Name) (type : Lean.Expr) (val : Lean.Expr) :
Equations
@[export lean_local_decl_binder_info]
Equations
• = match x with | Lean.LocalDecl.cdecl index fvarId userName type bi kind => bi | x => Lean.BinderInfo.default
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations

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

Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
• fvarIdToDecl :
• decls :

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.
Equations
• One or more equations did not get rendered due to their size.
@[export lean_local_ctx_is_empty]
Equations

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.
def Lean.LocalContext.mkLetDecl (lctx : Lean.LocalContext) (fvarId : Lean.FVarId) (userName : Lean.Name) (type : Lean.Expr) (value : Lean.Expr) (nonDep : ) (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.

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.
@[export lean_local_ctx_find]
Equations
Equations
• One or more equations did not get rendered due to their size.

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

Equations

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

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

Return all of the free variables in the given context.

Equations
@[export lean_local_ctx_erase]
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
@[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.
@[export lean_local_ctx_num_indices]
Equations
• = lctx.decls.size
@[specialize #[]]
def Lean.LocalContext.foldlM {m : Type u_1 → Type u_2} {β : Type u_1} [inst : ] (lctx : Lean.LocalContext) (f : βLean.LocalDeclm β) (init : β) (start : ) :
m β
Equations
• One or more equations did not get rendered due to their size.
@[specialize #[]]
def Lean.LocalContext.foldrM {m : Type u_1 → Type u_2} {β : Type u_1} [inst : ] (lctx : Lean.LocalContext) (f : Lean.LocalDeclβm β) (init : β) :
m β
Equations
@[specialize #[]]
def Lean.LocalContext.forM {m : Type u_1 → Type u_2} [inst : ] (lctx : Lean.LocalContext) (f : ) :
Equations
@[specialize #[]]
def Lean.LocalContext.findDeclM? {m : Type u_1 → Type u_2} {β : Type u_1} [inst : ] (lctx : Lean.LocalContext) (f : Lean.LocalDeclm ()) :
m ()
Equations
@[specialize #[]]
def Lean.LocalContext.findDeclRevM? {m : Type u_1 → Type u_2} {β : Type u_1} [inst : ] (lctx : Lean.LocalContext) (f : Lean.LocalDeclm ()) :
m ()
Equations
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 : β) (init : β) (start : ) :
β
Equations
@[inline]
def Lean.LocalContext.foldr {β : Type u_1} (lctx : Lean.LocalContext) (f : Lean.LocalDeclββ) (init : β) :
β
Equations
Equations
@[inline]
def Lean.LocalContext.findDecl? {β : Type u_1} (lctx : Lean.LocalContext) (f : ) :
Equations
@[inline]
def Lean.LocalContext.findDeclRev? {β : Type u_1} (lctx : Lean.LocalContext) (f : ) :
Equations
partial def Lean.LocalContext.isSubPrefixOfAux (a₁ : ) (a₂ : ) (exceptFVars : ) (i : Nat) (j : Nat) :
def Lean.LocalContext.isSubPrefixOf (lctx₁ : Lean.LocalContext) (lctx₂ : Lean.LocalContext) (exceptFVars : optParam () #[]) :

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
@[inline]
def Lean.LocalContext.mkBinding (isLambda : Bool) (lctx : Lean.LocalContext) (xs : ) (b : Lean.Expr) :
Equations
• One or more equations did not get rendered due to their size.

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

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

Equations
@[inline]
def Lean.LocalContext.anyM {m : TypeType u_1} [inst : ] (lctx : Lean.LocalContext) (p : ) :
Equations
@[inline]
def Lean.LocalContext.allM {m : TypeType u_1} [inst : ] (lctx : Lean.LocalContext) (p : ) :
Equations
@[inline]

Return true if lctx contains a local declaration satisfying p.

Equations
@[inline]

Return true if all declarations in lctx satisfy p.

Equations

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.
class Lean.MonadLCtx (m : ) :
• getLCtx :

Class used to denote that m has a local context.

Instances
instance Lean.instMonadLCtx {m : } {n : } [inst : ] [inst : ] :
Equations
• Lean.instMonadLCtx = { getLCtx := liftM Lean.getLCtx }
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.