inductive Lean.LocalDecl : Type

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

Equations

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

@[export lean_mk_local_decl]

def Lean.mkLocalDeclEx (index : Nat) (fvarId : Lean.FVarId) (userName : Lean.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

@[export lean_mk_let_decl]

def Lean.mkLetDeclEx (index : Nat) (fvarId : Lean.FVarId) (userName : Lean.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

@[export lean_local_decl_binder_info]

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

Equations

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

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

Equations

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

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

Equations

• Lean.LocalDecl.index _fun_discr = match _fun_discr with | Lean.LocalDecl.cdecl i fvarId userName type bi => i | Lean.LocalDecl.ldecl i fvarId userName type value nonDep => 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 _fun_discr = match _fun_discr with | Lean.LocalDecl.cdecl index id userName type bi => id | Lean.LocalDecl.ldecl index id userName type value nonDep => id

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

Equations

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

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

Equations

• Lean.LocalDecl.type _fun_discr = match _fun_discr with | Lean.LocalDecl.cdecl index fvarId userName t bi => t | Lean.LocalDecl.ldecl index fvarId userName t value nonDep => 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.isAuxDecl (d : Lean.LocalDecl) : Bool

Equations

• Lean.LocalDecl.isAuxDecl d = Lean.BinderInfo.isAuxDecl (Lean.LocalDecl.binderInfo d)

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

Equations

• Lean.LocalDecl.value? _fun_discr = match _fun_discr with | Lean.LocalDecl.cdecl index fvarId userName type bi => none | Lean.LocalDecl.ldecl index fvarId userName type v nonDep => 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

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

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

Equations

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

def Lean.LocalDecl.setUserName : Lean.LocalDecl → Lean.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

• 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

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

@[export lean_local_ctx_mk_local_decl]

def Lean.LocalContext.mkLocalDecl (lctx : Lean.LocalContext) (fvarId : Lean.FVarId) (userName : Lean.Name) (type : Lean.Expr) (bi : optParam Lean.BinderInfo Lean.BinderInfo.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.

@[export lean_local_ctx_mk_let_decl]

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

Equations

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

def Lean.LocalContext.getUnusedName (lctx : Lean.LocalContext) (suggestion : Lean.Name) : Lean.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 : Lean.Name) : Lean.LocalContext

Equations

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

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

Equations

• Lean.LocalContext.foldrM lctx f init = Lean.PersistentArray.foldrM lctx.decls (fun decl b => match decl with | none => pure b | some decl => f decl b) init

@[specialize #[]]

def Lean.LocalContext.forM {m : Type u_1 → Type u_2} [inst : 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 => 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} [inst : 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 => 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} [inst : Monad m] (lctx : Lean.LocalContext) (f : Lean.LocalDecl → m (Option β)) : m (Option β)

Equations

• Lean.LocalContext.findDeclRevM? lctx f = Lean.PersistentArray.findSomeRevM? lctx.decls fun decl => match decl with | none => pure none | some decl => f decl

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 x => 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} [inst : 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 => match d with | some decl => p decl | none => pure false

@[inline]

def Lean.LocalContext.allM {m : Type → Type u_1} [inst : 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 => 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

• getLCtx : m Lean.LocalContext

Class used to denote that m has a local context.

instance Lean.instMonadLCtx {m : Type → Type} {n : Type → Type} [inst : MonadLift m n] [inst : 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.