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 : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯

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

• x.binderInfoEx = 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

• x.isLet = 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

• x.index = 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

• x.fvarId = 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

• x.userName = 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

• x.type = 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

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

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

Equations

• x.kind = 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

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

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

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

Equations

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

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

Equations

• x.value? = 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

• x.hasValue = 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

• x✝.setValue 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

• decl.toExpr = Lean.mkFVar decl.fvarId

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

Equations

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

def Lean.LocalDecl.setKind : Lean.LocalDecl → Lean.LocalDeclKind → Lean.LocalDecl

Set the kind of a LocalDecl.

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

• lctx.isEmpty = lctx.fvarIdToDecl.isEmpty

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

• lctx.find? fvarId = lctx.fvarIdToDecl.find? fvarId

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

Equations

• lctx.findFVar? e = lctx.find? e.fvarId!

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

Equations

• lctx.get! fvarId = match lctx.find? fvarId with | some d => d | none => panicWithPosWithDecl "Lean.LocalContext" "Lean.LocalContext.get!" 227 14 "unknown free variable"

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

• lctx.getFVar! e = lctx.get! e.fvarId!

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

Equations

• lctx.contains fvarId = lctx.fvarIdToDecl.contains 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

• lctx.containsFVar e = lctx.contains e.fvarId!

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

Equations

• lctx.getFVarIds = lctx.decls.foldl (fun (r : Array Lean.FVarId) (decl? : Option Lean.LocalDecl) => match decl? with | some decl => r.push decl.fvarId | none => r) #[]

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

Return all of the free variables in the given context.

Equations

• lctx.getFVars = Array.map Lean.mkFVar lctx.getFVarIds

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

• lctx.usesUserName userName = (lctx.findFromUserName? userName).isSome

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

• lctx.lastDecl = lctx.decls.get! (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.setKind (lctx : Lean.LocalContext) (fvarId : Lean.FVarId) (kind : Lean.LocalDeclKind) : Lean.LocalContext

Set the kind of the given fvar.

Equations

• lctx.setKind fvarId kind = lctx.modifyLocalDecl fvarId fun (x : Lean.LocalDecl) => x.setKind kind

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

Equations

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

@[export lean_local_ctx_num_indices]

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

Equations

• lctx.numIndices = lctx.decls.size

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

Equations

• lctx.getAt? i = lctx.decls.get! 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

• lctx.foldlM f init start = lctx.decls.foldlM (fun (b : β) (decl : Option Lean.LocalDecl) => match decl with | none => pure b | some decl => f b decl) init start

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

• lctx.foldrM f init = lctx.decls.foldrM (fun (decl : Option Lean.LocalDecl) (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} [Monad m] (lctx : Lean.LocalContext) (f : Lean.LocalDecl → m PUnit) : m PUnit

Equations

• lctx.forM f = lctx.decls.forM 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

• lctx.findDeclM? f = lctx.decls.findSomeM? 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

• lctx.findDeclRevM? f = lctx.decls.findSomeRevM? fun (decl : Option Lean.LocalDecl) => match decl with | none => pure none | some decl => f decl

instance Lean.LocalContext.instForInLocalDecl {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

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

@[inline]

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

Equations

• lctx.foldr f init = (lctx.foldrM f init).run

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

Equations

• lctx.size = lctx.foldl (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

• lctx.findDecl? f = (lctx.findDeclM? f).run

@[inline]

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

Equations

• lctx.findDeclRev? f = (lctx.findDeclRevM? f).run

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

• lctx₁.isSubPrefixOf 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

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

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

• lctx.anyM p = lctx.decls.anyM 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

• lctx.allM p = lctx.decls.allM 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

• lctx.any p = (lctx.anyM p).run

@[inline]

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

Return true if all declarations in lctx satisfy p.

Equations

• lctx.all p = (lctx.allM p).run

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.

def Lean.LocalContext.getRoundtrippingUserName? (lctx : Lean.LocalContext) (fvarId : Lean.FVarId) : Option Lake.Name

Given an FVarId, this function returns the corresponding user name, but only if the name can be used to recover the original FVarId.

Equations

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

def Lean.LocalContext.sortFVarsByContextOrder (lctx : Lean.LocalContext) (hyps : Array Lean.FVarId) : Array Lean.FVarId

Sort the given FVarIds by the order in which they appear in lctx. If any of the FVarIds do not appear in lctx, the result is unspecified.

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

Equations

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

def Lean.getLocalHyps {m : Type → Type} [Monad m] [Lean.MonadLCtx m] : m (Array Lean.Expr)

Return local hypotheses which are not "implementation detail", as Exprs.

Equations

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

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.