inductive Lean.LocalDeclKind : Type

• 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 : Nat → Nat 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.

instance Lean.instInhabitedLocalDeclKind : Inhabited Lean.LocalDeclKind

instance Lean.instReprLocalDeclKind : Repr Lean.LocalDeclKind

instance Lean.instDecidableEqLocalDeclKind : DecidableEq Lean.LocalDeclKind

instance Lean.instHashableLocalDeclKind : Hashable Lean.LocalDeclKind

inductive Lean.LocalDecl : Type

• cdecl: Nat → Lean.FVarId → Lake.Name → Lean.Expr → Lean.BinderInfo → Lean.LocalDeclKind → Lean.LocalDecl
• ldecl: Nat → Lean.FVarId → Lake.Name → Lean.Expr → Lean.Expr → Bool → Lean.LocalDeclKind → 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.

instance Lean.instInhabitedLocalDecl : Inhabited Lean.LocalDecl

@[export lean_mk_local_decl]

def Lean.mkLocalDeclEx (index : Nat) (fvarId : Lean.FVarId) (userName : Lake.Name) (type : Lean.Expr) (bi : Lean.BinderInfo) : Lean.LocalDecl

@[export lean_mk_let_decl]

def Lean.mkLetDeclEx (index : Nat) (fvarId : Lean.FVarId) (userName : Lake.Name) (type : Lean.Expr) (val : Lean.Expr) : Lean.LocalDecl

@[export lean_local_decl_binder_info]

def Lean.LocalDecl.binderInfoEx : Lean.LocalDecl → Lean.BinderInfo

def Lean.LocalDecl.isLet : Lean.LocalDecl → Bool

def Lean.LocalDecl.index : Lean.LocalDecl → Nat

def Lean.LocalDecl.setIndex : Lean.LocalDecl → Nat → Lean.LocalDecl

def Lean.LocalDecl.fvarId : Lean.LocalDecl → Lean.FVarId

def Lean.LocalDecl.userName : Lean.LocalDecl → Lake.Name

def Lean.LocalDecl.type : Lean.LocalDecl → Lean.Expr

def Lean.LocalDecl.setType : Lean.LocalDecl → Lean.Expr → Lean.LocalDecl

def Lean.LocalDecl.binderInfo : Lean.LocalDecl → Lean.BinderInfo

def Lean.LocalDecl.kind : Lean.LocalDecl → Lean.LocalDeclKind

def Lean.LocalDecl.isAuxDecl (d : Lean.LocalDecl) : Bool

def Lean.LocalDecl.isImplementationDetail (d : Lean.LocalDecl) : Bool

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

def Lean.LocalDecl.value? : Lean.LocalDecl → Option Lean.Expr

def Lean.LocalDecl.value : Lean.LocalDecl → Lean.Expr

def Lean.LocalDecl.hasValue : Lean.LocalDecl → Bool

def Lean.LocalDecl.setValue : Lean.LocalDecl → Lean.Expr → Lean.LocalDecl

def Lean.LocalDecl.setUserName : Lean.LocalDecl → Lake.Name → Lean.LocalDecl

def Lean.LocalDecl.setBinderInfo : Lean.LocalDecl → Lean.BinderInfo → Lean.LocalDecl

def Lean.LocalDecl.toExpr (decl : Lean.LocalDecl) : Lean.Expr

def Lean.LocalDecl.hasExprMVar : Lean.LocalDecl → Bool

structure Lean.LocalContext : Type

• fvarIdToDecl : Lean.PersistentHashMap Lean.FVarId Lean.LocalDecl
• decls : Lean.PersistentArray (Option Lean.LocalDecl)

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.

instance Lean.instInhabitedLocalContext : Inhabited Lean.LocalContext

@[export lean_mk_empty_local_ctx]

def Lean.LocalContext.mkEmpty : Unit → Lean.LocalContext

def Lean.LocalContext.empty : Lean.LocalContext

@[export lean_local_ctx_is_empty]

def Lean.LocalContext.isEmpty (lctx : Lean.LocalContext) : Bool

def Lean.LocalContext.mkLocalDecl (lctx : Lean.LocalContext) (fvarId : Lean.FVarId) (userName : Lake.Name) (type : Lean.Expr) (bi : optParam Lean.BinderInfo Lean.BinderInfo.default) (kind : optParam Lean.LocalDeclKind Lean.LocalDeclKind.default) : Lean.LocalContext

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.

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) : Lean.LocalContext

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

def Lean.LocalContext.addDecl (lctx : Lean.LocalContext) (newDecl : Lean.LocalDecl) : Lean.LocalContext

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

@[export lean_local_ctx_find]

def Lean.LocalContext.find? (lctx : Lean.LocalContext) (fvarId : Lean.FVarId) : Option Lean.LocalDecl

def Lean.LocalContext.findFVar? (lctx : Lean.LocalContext) (e : Lean.Expr) : Option Lean.LocalDecl

def Lean.LocalContext.get! (lctx : Lean.LocalContext) (fvarId : Lean.FVarId) : Lean.LocalDecl

def Lean.LocalContext.getFVar! (lctx : Lean.LocalContext) (e : Lean.Expr) : Lean.LocalDecl

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

def Lean.LocalContext.contains (lctx : Lean.LocalContext) (fvarId : Lean.FVarId) : Bool

def Lean.LocalContext.containsFVar (lctx : Lean.LocalContext) (e : Lean.Expr) : Bool

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

def Lean.LocalContext.getFVarIds (lctx : Lean.LocalContext) : Array Lean.FVarId

def Lean.LocalContext.getFVars (lctx : Lean.LocalContext) : Array Lean.Expr

Return all of the free variables in the given context.

@[export lean_local_ctx_erase]

def Lean.LocalContext.erase (lctx : Lean.LocalContext) (fvarId : Lean.FVarId) : Lean.LocalContext

def Lean.LocalContext.pop (lctx : Lean.LocalContext) : Lean.LocalContext

def Lean.LocalContext.findFromUserName? (lctx : Lean.LocalContext) (userName : Lake.Name) : Option Lean.LocalDecl

def Lean.LocalContext.usesUserName (lctx : Lean.LocalContext) (userName : Lake.Name) : Bool

def Lean.LocalContext.getUnusedName (lctx : Lean.LocalContext) (suggestion : Lake.Name) : Lake.Name

def Lean.LocalContext.lastDecl (lctx : Lean.LocalContext) : Option Lean.LocalDecl

def Lean.LocalContext.setUserName (lctx : Lean.LocalContext) (fvarId : Lean.FVarId) (userName : Lake.Name) : Lean.LocalContext

def Lean.LocalContext.renameUserName (lctx : Lean.LocalContext) (fromName : Lake.Name) (toName : Lake.Name) : Lean.LocalContext

@[inline]

def Lean.LocalContext.modifyLocalDecl (lctx : Lean.LocalContext) (fvarId : Lean.FVarId) (f : Lean.LocalDecl → Lean.LocalDecl) : Lean.LocalContext

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.

def Lean.LocalContext.setBinderInfo (lctx : Lean.LocalContext) (fvarId : Lean.FVarId) (bi : Lean.BinderInfo) : Lean.LocalContext

@[export lean_local_ctx_num_indices]

def Lean.LocalContext.numIndices (lctx : Lean.LocalContext) : Nat

def Lean.LocalContext.getAt? (lctx : Lean.LocalContext) (i : Nat) : Option Lean.LocalDecl

@[specialize #[]]

def Lean.LocalContext.foldlM {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (lctx : Lean.LocalContext) (f : β → Lean.LocalDecl → m β) (init : β) (start : optParam Nat 0) : m β

@[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 β

@[specialize #[]]

def Lean.LocalContext.forM {m : Type u_1 → Type u_2} [Monad m] (lctx : Lean.LocalContext) (f : Lean.LocalDecl → m PUnit) : m PUnit

@[specialize #[]]

def Lean.LocalContext.findDeclM? {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (lctx : Lean.LocalContext) (f : Lean.LocalDecl → m (Option β)) : m (Option β)

@[specialize #[]]

def Lean.LocalContext.findDeclRevM? {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (lctx : Lean.LocalContext) (f : Lean.LocalDecl → m (Option β)) : m (Option β)

instance Lean.LocalContext.instForInLocalContextLocalDecl {m : Type u_1 → Type u_2} : ForIn m Lean.LocalContext Lean.LocalDecl

@[inline]

def Lean.LocalContext.foldl {β : Type u_1} (lctx : Lean.LocalContext) (f : β → Lean.LocalDecl → β) (init : β) (start : optParam Nat 0) : β

@[inline]

def Lean.LocalContext.foldr {β : Type u_1} (lctx : Lean.LocalContext) (f : Lean.LocalDecl → β → β) (init : β) : β

def Lean.LocalContext.size (lctx : Lean.LocalContext) : Nat

@[inline]

def Lean.LocalContext.findDecl? {β : Type u_1} (lctx : Lean.LocalContext) (f : Lean.LocalDecl → Option β) : Option β

@[inline]

def Lean.LocalContext.findDeclRev? {β : Type u_1} (lctx : Lean.LocalContext) (f : Lean.LocalDecl → Option β) : Option β

partial def Lean.LocalContext.isSubPrefixOfAux (a₁ : Lean.PArray (Option Lean.LocalDecl)) (a₂ : Lean.PArray (Option Lean.LocalDecl)) (exceptFVars : Array Lean.Expr) (i : Nat) (j : Nat) : Bool

def Lean.LocalContext.isSubPrefixOf (lctx₁ : Lean.LocalContext) (lctx₂ : Lean.LocalContext) (exceptFVars : optParam (Array Lean.Expr) #[]) : Bool

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.

@[inline]

def Lean.LocalContext.mkBinding (isLambda : Bool) (lctx : Lean.LocalContext) (xs : Array Lean.Expr) (b : Lean.Expr) : Lean.Expr

def Lean.LocalContext.mkLambda (lctx : Lean.LocalContext) (xs : Array Lean.Expr) (b : Lean.Expr) : Lean.Expr

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

def Lean.LocalContext.mkForall (lctx : Lean.LocalContext) (xs : Array Lean.Expr) (b : Lean.Expr) : Lean.Expr

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

@[inline]

def Lean.LocalContext.anyM {m : Type → Type u_1} [Monad m] (lctx : Lean.LocalContext) (p : Lean.LocalDecl → m Bool) : m Bool

@[inline]

def Lean.LocalContext.allM {m : Type → Type u_1} [Monad m] (lctx : Lean.LocalContext) (p : Lean.LocalDecl → m Bool) : m Bool

@[inline]

def Lean.LocalContext.any (lctx : Lean.LocalContext) (p : Lean.LocalDecl → Bool) : Bool

Return true if lctx contains a local declaration satisfying p.

@[inline]

def Lean.LocalContext.all (lctx : Lean.LocalContext) (p : Lean.LocalDecl → Bool) : Bool

Return true if all declarations in lctx satisfy p.

def Lean.LocalContext.sanitizeNames (lctx : Lean.LocalContext) : StateM Lean.NameSanitizerState Lean.LocalContext

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

class Lean.MonadLCtx (m : Type → Type) : Type

• getLCtx : m Lean.LocalContext

Class used to denote that m has a local context.

instance Lean.instMonadLCtx {m : Type → Type} {n : Type → Type} [MonadLift m n] [Lean.MonadLCtx m] : Lean.MonadLCtx n

def Lean.LocalDecl.replaceFVarId (fvarId : Lean.FVarId) (e : Lean.Expr) (d : Lean.LocalDecl) : Lean.LocalDecl

def Lean.LocalContext.replaceFVarId (fvarId : Lean.FVarId) (e : Lean.Expr) (lctx : Lean.LocalContext) : Lean.LocalContext