inductive Lean.LocalDeclKind : Type

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

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

Instances For

• Lean.instHashableLocalDeclKind
• Lean.instInhabitedLocalDeclKind
• Lean.instReprLocalDeclKind

instance Lean.instInhabitedLocalDeclKind : Inhabited LocalDeclKind

Equations

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

instance Lean.instReprLocalDeclKind : Repr LocalDeclKind

Equations

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

instance Lean.instDecidableEqLocalDeclKind : DecidableEq LocalDeclKind

Equations

• Lean.instDecidableEqLocalDeclKind x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance Lean.instHashableLocalDeclKind : Hashable 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.

See LocalDecl.index, LocalDecl.fvarId, LocalDecl.userName, LocalDecl.type for accessors for arguments common to both constructors.

• cdecl (index : Nat) (fvarId : FVarId) (userName : Name) (type : Expr) (bi : BinderInfo) (kind : LocalDeclKind) : LocalDecl

  A local variable.

• ldecl (index : Nat) (fvarId : FVarId) (userName : Name) (type value : Expr) (nonDep : Bool) (kind : LocalDeclKind) : LocalDecl

  A let-bound free variable, with a value : Expr.

Instances For

• Lean.LocalContext.instForInLocalDecl
• Lean.instInhabitedLocalDecl

instance Lean.instInhabitedLocalDecl : Inhabited 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 : FVarId) (userName : Name) (type : Expr) (bi : BinderInfo) : 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 : FVarId) (userName : Name) (type val : Expr) : 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 : LocalDecl → BinderInfo

Equations

• (Lean.LocalDecl.cdecl index fvarId userName type bi kind).binderInfoEx = bi
• x✝.binderInfoEx = Lean.BinderInfo.default

def Lean.LocalDecl.isLet : LocalDecl → Bool

Equations

• (Lean.LocalDecl.cdecl index fvarId userName type bi kind).isLet = false
• (Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind).isLet = true

def Lean.LocalDecl.index : LocalDecl → Nat

The position of the decl in the local context.

Equations

• (Lean.LocalDecl.cdecl index fvarId userName type bi kind).index = index
• (Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind).index = index

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

Equations

• (Lean.LocalDecl.cdecl index id n t bi k).setIndex x✝ = Lean.LocalDecl.cdecl x✝ id n t bi k
• (Lean.LocalDecl.ldecl index id n t v nd k).setIndex x✝ = Lean.LocalDecl.ldecl x✝ id n t v nd k

def Lean.LocalDecl.fvarId : LocalDecl → FVarId

The unique id of the free variable.

Equations

• (Lean.LocalDecl.cdecl index fvarId userName type bi kind).fvarId = fvarId
• (Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind).fvarId = fvarId

def Lean.LocalDecl.userName : LocalDecl → Name

The pretty-printable name of the variable.

Equations

• (Lean.LocalDecl.cdecl index fvarId userName type bi kind).userName = userName
• (Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind).userName = userName

def Lean.LocalDecl.type : LocalDecl → Expr

The type of the variable.

Equations

• (Lean.LocalDecl.cdecl index fvarId userName type bi kind).type = type
• (Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind).type = type

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

Equations

• (Lean.LocalDecl.cdecl idx id n type bi k).setType x✝ = Lean.LocalDecl.cdecl idx id n x✝ bi k
• (Lean.LocalDecl.ldecl idx id n type v nd k).setType x✝ = Lean.LocalDecl.ldecl idx id n x✝ v nd k

def Lean.LocalDecl.binderInfo : LocalDecl → BinderInfo

Equations

• (Lean.LocalDecl.cdecl index fvarId userName type bi kind).binderInfo = bi
• (Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind).binderInfo = Lean.BinderInfo.default

def Lean.LocalDecl.kind : LocalDecl → LocalDeclKind

Equations

• (Lean.LocalDecl.cdecl index fvarId userName type bi kind).kind = kind
• (Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind).kind = kind

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

Equations

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

def Lean.LocalDecl.isImplementationDetail (d : 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? : LocalDecl → Option Expr

Equations

• (Lean.LocalDecl.cdecl index fvarId userName type bi kind).value? = none
• (Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind).value? = some value

def Lean.LocalDecl.value : LocalDecl → Expr

Equations

• (Lean.LocalDecl.cdecl index fvarId userName type bi kind).value = panicWithPosWithDecl "Lean.LocalContext" "Lean.LocalDecl.value" 123 29 "let declaration expected"
• (Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind).value = value

def Lean.LocalDecl.hasValue : LocalDecl → Bool

Equations

• (Lean.LocalDecl.cdecl index fvarId userName type bi kind).hasValue = false
• (Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind).hasValue = true

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

Equations

• (Lean.LocalDecl.ldecl idx id n t value nd k).setValue x✝ = Lean.LocalDecl.ldecl idx id n t x✝ nd k
• x✝¹.setValue x✝ = x✝¹

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

Equations

• (Lean.LocalDecl.cdecl index id userName type bi k).setUserName x✝ = Lean.LocalDecl.cdecl index id x✝ type bi k
• (Lean.LocalDecl.ldecl index id userName type val nd k).setUserName x✝ = Lean.LocalDecl.ldecl index id x✝ type val nd k

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

Equations

• (Lean.LocalDecl.cdecl index id n type bi k).setBinderInfo x✝ = Lean.LocalDecl.cdecl index id n type x✝ k
• (Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind).setBinderInfo x✝ = panicWithPosWithDecl "Lean.LocalContext" "Lean.LocalDecl.setBinderInfo" 140 38 "unexpected let declaration"

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

Equations

• decl.toExpr = Lean.mkFVar decl.fvarId

def Lean.LocalDecl.hasExprMVar : LocalDecl → Bool

Equations

• (Lean.LocalDecl.cdecl index fvarId userName type bi kind).hasExprMVar = type.hasExprMVar
• (Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind).hasExprMVar = (type.hasExprMVar || value.hasExprMVar)

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

Set the kind of a LocalDecl.

Equations

• (Lean.LocalDecl.cdecl index fvarId userName type bi kind).setKind x✝ = Lean.LocalDecl.cdecl index fvarId userName type bi x✝
• (Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind).setKind x✝ = Lean.LocalDecl.ldecl index fvarId userName type value nonDep x✝

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. It also maps free variables corresponding to auxiliary declarations (recursive references and where and let rec bindings) to their fully-qualified global names.

When inspecting a goal or expected type in the infoview, the local context is all of the variables above the ⊢ symbol.

• fvarIdToDecl : PersistentHashMap FVarId LocalDecl
• decls : PersistentArray (Option LocalDecl)
• auxDeclToFullName : FVarIdMap Name

Instances For

• Lean.LocalContext.instForInLocalDecl
• Lean.Widget.instTypeNameLocalContext
• Lean.instInhabitedLocalContext

instance Lean.instInhabitedLocalContext : Inhabited LocalContext

Equations

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

@[export lean_mk_empty_local_ctx]

def Lean.LocalContext.mkEmpty : Unit → LocalContext

Equations

• Lean.LocalContext.mkEmpty x✝ = { }

def Lean.LocalContext.empty : LocalContext

Equations

• Lean.LocalContext.empty = { }

@[export lean_local_ctx_is_empty]

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

Equations

• lctx.isEmpty = lctx.fvarIdToDecl.isEmpty

def Lean.LocalContext.mkLocalDecl (lctx : LocalContext) (fvarId : FVarId) (userName : Name) (type : Expr) (bi : BinderInfo := BinderInfo.default) (kind : LocalDeclKind := LocalDeclKind.default) : 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 : LocalContext) (fvarId : FVarId) (userName : Name) (type value : Expr) (nonDep : Bool := false) (kind : LocalDeclKind := default) : 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.mkAuxDecl (lctx : LocalContext) (fvarId : FVarId) (userName : Name) (type : Expr) (fullName : Name) : LocalContext

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

Equations

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

def Lean.LocalContext.addDecl (lctx : LocalContext) (newDecl : LocalDecl) : 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 : LocalContext) (fvarId : FVarId) : Option LocalDecl

Equations

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

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

Equations

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

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

Equations

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

def Lean.LocalContext.getFVar! (lctx : LocalContext) (e : Expr) : 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 : LocalContext) (fvarId : FVarId) : Bool

Equations

• lctx.contains fvarId = lctx.fvarIdToDecl.contains fvarId

def Lean.LocalContext.containsFVar (lctx : LocalContext) (e : 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 : LocalContext) : Array 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 : LocalContext) : Array 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 : LocalContext) (fvarId : FVarId) : LocalContext

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• lctx.lastDecl = lctx.decls[lctx.decls.size - 1]!

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

Equations

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

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

Equations

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

@[inline]

def Lean.LocalContext.modifyLocalDecl (lctx : LocalContext) (fvarId : FVarId) (f : LocalDecl → LocalDecl) : 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 : LocalContext) (fvarId : FVarId) (kind : LocalDeclKind) : 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 : LocalContext) (fvarId : FVarId) (bi : BinderInfo) : 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 : LocalContext) : Nat

Equations

• lctx.numIndices = lctx.decls.size

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

Equations

• lctx.getAt? i = lctx.decls[i]!

@[specialize #[]]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

def Lean.LocalContext.size (lctx : 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 : LocalContext) (f : LocalDecl → Option β) : Option β

Equations

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

@[inline]

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

Equations

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

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

def Lean.LocalContext.isSubPrefixOf (lctx₁ lctx₂ : LocalContext) (exceptFVars : Array 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 : LocalContext) (xs : Array Expr) (b : Expr) : Expr

Equations

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

def Lean.LocalContext.mkLambda (lctx : LocalContext) (xs : Array Expr) (b : Expr) : 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 : LocalContext) (xs : Array Expr) (b : Expr) : 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 : LocalContext) (p : 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 : LocalContext) (p : 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 : LocalContext) (p : 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 : LocalContext) (p : 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 : LocalContext) : StateM NameSanitizerState 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 : LocalContext) (fvarId : FVarId) : Option 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 : LocalContext) (hyps : Array FVarId) : Array 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 LocalContext

Instances

• Lean.Meta.instMonadLCtxMetaM
• Lean.instMonadLCtxOfMonadLift

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

Equations

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

def Lean.getLocalHyps {m : Type → Type} [Monad m] [MonadLCtx m] : m (Array 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 : FVarId) (e : Expr) (d : LocalDecl) : LocalDecl

Equations

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

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

Equations

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