inductive Lean.LocalDeclKind : Type

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

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

instance Lean.instInhabitedLocalDeclKind : Inhabited Lean.LocalDeclKind

Equations

• Lean.instInhabitedLocalDeclKind = { default := Lean.LocalDeclKind.default }

instance Lean.instReprLocalDeclKind : Repr Lean.LocalDeclKind

Equations

• Lean.instReprLocalDeclKind = { reprPrec := Lean.reprLocalDeclKind✝ }

instance Lean.instDecidableEqLocalDeclKind : DecidableEq Lean.LocalDeclKind

Equations

• Lean.instDecidableEqLocalDeclKind x y = if h : Lean.LocalDeclKind.toCtorIdx x = Lean.LocalDeclKind.toCtorIdx y then isTrue (_ : x = y) else isFalse (_ : x = y → False)

instance Lean.instHashableLocalDeclKind : Hashable Lean.LocalDeclKind

Equations

• Lean.instHashableLocalDeclKind = { hash := Lean.hashLocalDeclKind✝ }

inductive Lean.LocalDecl : Type

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.

• 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

instance Lean.instInhabitedLocalDecl : Inhabited Lean.LocalDecl

Equations

• Lean.instInhabitedLocalDecl = { default := Lean.LocalDecl.cdecl default default default default default default }

@[export lean_mk_local_decl]

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

Equations

• Lean.mkLocalDeclEx index fvarId userName type bi = Lean.LocalDecl.cdecl index fvarId userName type bi Lean.LocalDeclKind.default

@[export lean_mk_let_decl]

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

Equations

• Lean.mkLetDeclEx index fvarId userName type val = Lean.LocalDecl.ldecl index fvarId userName type val false Lean.LocalDeclKind.default

@[export lean_local_decl_binder_info]

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

Equations

• Lean.LocalDecl.binderInfoEx x = match x with | Lean.LocalDecl.cdecl index fvarId userName type bi kind => bi | x => Lean.BinderInfo.default

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

Equations

• Lean.LocalDecl.isLet x = match x with | Lean.LocalDecl.cdecl index fvarId userName type bi kind => false | Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind => true

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

Equations

• Lean.LocalDecl.index x = match x with | Lean.LocalDecl.cdecl i fvarId userName type bi kind => i | Lean.LocalDecl.ldecl i fvarId userName type value nonDep kind => i

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

Equations

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

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

Equations

• Lean.LocalDecl.fvarId x = match x with | Lean.LocalDecl.cdecl index id userName type bi kind => id | Lean.LocalDecl.ldecl index id userName type value nonDep kind => id

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

Equations

• Lean.LocalDecl.userName x = match x with | Lean.LocalDecl.cdecl index fvarId n type bi kind => n | Lean.LocalDecl.ldecl index fvarId n type value nonDep kind => n

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

Equations

• Lean.LocalDecl.type x = match x with | Lean.LocalDecl.cdecl index fvarId userName t bi kind => t | Lean.LocalDecl.ldecl index fvarId userName t value nonDep kind => t

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

Equations

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

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

Equations

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

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

Equations

• Lean.LocalDecl.kind x = match x with | Lean.LocalDecl.cdecl index fvarId userName type bi kind => kind | Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind => kind

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

Equations

• Lean.LocalDecl.isAuxDecl d = decide (Lean.LocalDecl.kind d = Lean.LocalDeclKind.auxDecl)

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

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

Equations

• Lean.LocalDecl.isImplementationDetail d = (Lean.LocalDecl.kind d != Lean.LocalDeclKind.default)

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

Equations

• Lean.LocalDecl.value? x = match x with | Lean.LocalDecl.cdecl index fvarId userName type bi kind => none | Lean.LocalDecl.ldecl index fvarId userName type v nonDep kind => some v

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

Equations

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

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

Equations

• Lean.LocalDecl.hasValue x = match x with | Lean.LocalDecl.cdecl index fvarId userName type bi kind => false | Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind => true

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

Equations

• Lean.LocalDecl.setValue x✝ x = match x✝, x with | Lean.LocalDecl.ldecl idx id n t value nd k, v => Lean.LocalDecl.ldecl idx id n t v nd k | d, x => d

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

Equations

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

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

Equations

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

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

Equations

• Lean.LocalDecl.toExpr decl = Lean.mkFVar (Lean.LocalDecl.fvarId decl)

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

Equations

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

structure Lean.LocalContext : Type

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.

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

instance Lean.instInhabitedLocalContext : Inhabited Lean.LocalContext

Equations

• Lean.instInhabitedLocalContext = { default := { fvarIdToDecl := default, decls := default } }

@[export lean_mk_empty_local_ctx]

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

Equations

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

def Lean.LocalContext.empty : Lean.LocalContext

Equations

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

@[export lean_local_ctx_is_empty]

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

Equations

• Lean.LocalContext.isEmpty lctx = Lean.PersistentHashMap.isEmpty lctx.fvarIdToDecl

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.

Equations

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

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.

Equations

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

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

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]

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

Equations

• Lean.LocalContext.find? lctx fvarId = Lean.PersistentHashMap.find? lctx.fvarIdToDecl fvarId

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

Equations

• Lean.LocalContext.findFVar? lctx e = Lean.LocalContext.find? lctx (Lean.Expr.fvarId! e)

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

Equations

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

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.

Equations

• Lean.LocalContext.getFVar! lctx e = Lean.LocalContext.get! lctx (Lean.Expr.fvarId! e)

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

Equations

• Lean.LocalContext.contains lctx fvarId = Lean.PersistentHashMap.contains lctx.fvarIdToDecl fvarId

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.

Equations

• Lean.LocalContext.containsFVar lctx e = Lean.LocalContext.contains lctx (Lean.Expr.fvarId! e)

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

Equations

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

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

Return all of the free variables in the given context.

Equations

• Lean.LocalContext.getFVars lctx = Array.map Lean.mkFVar (Lean.LocalContext.getFVarIds lctx)

@[export lean_local_ctx_erase]

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.LocalContext.usesUserName lctx userName = Option.isSome (Lean.LocalContext.findFromUserName? lctx userName)

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

Equations

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

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

Equations

• Lean.LocalContext.lastDecl lctx = Lean.PersistentArray.get! lctx.decls (lctx.decls.size - 1)

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.LocalContext.setBinderInfo lctx fvarId bi = Lean.LocalContext.modifyLocalDecl lctx fvarId fun (decl : Lean.LocalDecl) => Lean.LocalDecl.setBinderInfo decl bi

@[export lean_local_ctx_num_indices]

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

Equations

• Lean.LocalContext.numIndices lctx = lctx.decls.size

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

Equations

• Lean.LocalContext.getAt? lctx i = Lean.PersistentArray.get! lctx.decls i

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

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} [Monad m] (lctx : Lean.LocalContext) (f : Lean.LocalDecl → β → m β) (init : β) : m β

Equations

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

@[specialize #[]]

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

Equations

• Lean.LocalContext.forM lctx f = Lean.PersistentArray.forM lctx.decls fun (decl : Option Lean.LocalDecl) => match decl with | none => pure PUnit.unit | some decl => f decl

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

Equations

• Lean.LocalContext.findDeclM? lctx f = Lean.PersistentArray.findSomeM? lctx.decls fun (decl : Option Lean.LocalDecl) => match decl with | none => pure none | some decl => f decl

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

Equations

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

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

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

• Lean.LocalContext.foldl lctx f init start = Id.run (Lean.LocalContext.foldlM lctx f init start)

@[inline]

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

Equations

• Lean.LocalContext.foldr lctx f init = Id.run (Lean.LocalContext.foldrM lctx f init)

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

Equations

• Lean.LocalContext.size lctx = Lean.LocalContext.foldl lctx (fun (n : Nat) (x : Lean.LocalDecl) => n + 1) 0

@[inline]

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

Equations

• Lean.LocalContext.findDecl? lctx f = Id.run (Lean.LocalContext.findDeclM? lctx f)

@[inline]

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

Equations

• Lean.LocalContext.findDeclRev? lctx f = Id.run (Lean.LocalContext.findDeclRevM? lctx f)

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.

Equations

• Lean.LocalContext.isSubPrefixOf lctx₁ lctx₂ exceptFVars = Lean.LocalContext.isSubPrefixOfAux lctx₁.decls lctx₂.decls exceptFVars 0 0

@[inline]

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

Equations

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

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

Equations

• Lean.LocalContext.mkLambda lctx xs b = Lean.LocalContext.mkBinding true lctx xs b

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ᵢ, αᵢ.

Equations

• Lean.LocalContext.mkForall lctx xs b = Lean.LocalContext.mkBinding false lctx xs b

@[inline]

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

Equations

• Lean.LocalContext.anyM lctx p = Lean.PersistentArray.anyM lctx.decls fun (d : Option Lean.LocalDecl) => match d with | some decl => p decl | none => pure false

@[inline]

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

Equations

• Lean.LocalContext.allM lctx p = Lean.PersistentArray.allM lctx.decls fun (d : Option Lean.LocalDecl) => match d with | some decl => p decl | none => pure true

@[inline]

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

Return true if lctx contains a local declaration satisfying p.

Equations

• Lean.LocalContext.any lctx p = Id.run (Lean.LocalContext.anyM lctx p)

@[inline]

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

Return true if all declarations in lctx satisfy p.

Equations

• Lean.LocalContext.all lctx p = Id.run (Lean.LocalContext.allM lctx 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.

Equations

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

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

Class used to denote that m has a local context.

• getLCtx : m Lean.LocalContext

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

Equations

• Lean.instMonadLCtx = { getLCtx := liftM Lean.getLCtx }

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

Equations

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

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

Equations

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