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
infun 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 tofoo >>= fun __tmp => pure (__tmp + bar)
, where__tmp
has theimplDetail
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 declarationfoo : Nat → Nat
to allow recursive calls. This declaration has theauxDecl
kind.
Equations
- Lean.instInhabitedLocalDeclKind = { default := Lean.LocalDeclKind.default }
Equations
- Lean.instReprLocalDeclKind = { reprPrec := Lean.reprLocalDeclKind✝ }
Equations
- Lean.instDecidableEqLocalDeclKind x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯
Equations
- Lean.instHashableLocalDeclKind = { hash := Lean.hashLocalDeclKind✝ }
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 contextfvarId
the unique id of the free variablesuserName
the pretty-printable name of the variabletype
the type. Acdecl
is a local variable, aldecl
is a let-bound free variable with avalue : Expr
.
- cdecl: Nat → Lean.FVarId → Lean.Name → Lean.Expr → Lean.BinderInfo → Lean.LocalDeclKind → Lean.LocalDecl
- ldecl: Nat → Lean.FVarId → Lean.Name → Lean.Expr → Lean.Expr → Bool → Lean.LocalDeclKind → Lean.LocalDecl
Equations
- Lean.instInhabitedLocalDecl = { default := Lean.LocalDecl.cdecl default default default default default default }
Equations
- Lean.mkLocalDeclEx index fvarId userName type bi = Lean.LocalDecl.cdecl index fvarId userName type bi Lean.LocalDeclKind.default
Equations
- Lean.mkLetDeclEx index fvarId userName type val = Lean.LocalDecl.ldecl index fvarId userName type val false Lean.LocalDeclKind.default
Equations
- (Lean.LocalDecl.cdecl index fvarId userName type bi kind).binderInfoEx = bi
- x.binderInfoEx = Lean.BinderInfo.default
Equations
- (Lean.LocalDecl.cdecl index fvarId userName type bi kind).isLet = false
- (Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind).isLet = true
Equations
- (Lean.LocalDecl.cdecl index fvarId userName type bi kind).index = index
- (Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind).index = index
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
Equations
- (Lean.LocalDecl.cdecl index fvarId userName type bi kind).fvarId = fvarId
- (Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind).fvarId = fvarId
Equations
- (Lean.LocalDecl.cdecl index fvarId userName type bi kind).userName = userName
- (Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind).userName = userName
Equations
- (Lean.LocalDecl.cdecl index fvarId userName type bi kind).type = type
- (Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind).type = type
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
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
Equations
- (Lean.LocalDecl.cdecl index fvarId userName type bi kind).kind = kind
- (Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind).kind = kind
Equations
- d.isAuxDecl = decide (d.kind = Lean.LocalDeclKind.auxDecl)
Is the local declaration an implementation-detail hypothesis (including auxiliary declarations)?
Equations
- d.isImplementationDetail = (d.kind != Lean.LocalDeclKind.default)
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
Equations
- (Lean.LocalDecl.cdecl index fvarId userName type bi kind).value = panicWithPosWithDecl "Lean.LocalContext" "Lean.LocalDecl.value" 120 29 "let declaration expected"
- (Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind).value = value
Equations
- (Lean.LocalDecl.cdecl index fvarId userName type bi kind).hasValue = false
- (Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind).hasValue = true
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✝
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
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" 137 38 "unexpected let declaration"
Equations
- decl.toExpr = Lean.mkFVar decl.fvarId
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)
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
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)
Equations
- Lean.instInhabitedLocalContext = { default := { fvarIdToDecl := default, decls := default } }
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- lctx.isEmpty = lctx.fvarIdToDecl.isEmpty
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.
Low level API for let declarations. Do not use directly.
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- lctx.find? fvarId = lctx.fvarIdToDecl.find? fvarId
Equations
- lctx.findFVar? e = lctx.find? e.fvarId!
Equations
- lctx.get! fvarId = match lctx.find? fvarId with | some d => d | none => panicWithPosWithDecl "Lean.LocalContext" "Lean.LocalContext.get!" 227 14 "unknown free variable"
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!
Equations
- lctx.contains fvarId = lctx.fvarIdToDecl.contains fvarId
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!
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) #[]
Return all of the free variables in the given context.
Equations
- lctx.getFVars = Array.map Lean.mkFVar lctx.getFVarIds
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- lctx.usesUserName userName = (lctx.findFromUserName? userName).isSome
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
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.
Set the kind of the given fvar.
Equations
- lctx.setKind fvarId kind = lctx.modifyLocalDecl fvarId fun (x : Lean.LocalDecl) => x.setKind kind
Equations
- lctx.setBinderInfo fvarId bi = lctx.modifyLocalDecl fvarId fun (decl : Lean.LocalDecl) => decl.setBinderInfo bi
Equations
- lctx.numIndices = lctx.decls.size
Equations
- lctx.getAt? i = lctx.decls.get! i
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
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
Equations
- lctx.forM f = lctx.decls.forM fun (decl : Option Lean.LocalDecl) => match decl with | none => pure PUnit.unit | some decl => f decl
Equations
- lctx.findDeclM? f = lctx.decls.findSomeM? fun (decl : Option Lean.LocalDecl) => match decl with | none => pure none | some decl => f decl
Equations
- lctx.findDeclRevM? f = lctx.decls.findSomeRevM? fun (decl : Option Lean.LocalDecl) => match decl with | none => pure none | some decl => f decl
Equations
- One or more equations did not get rendered due to their size.
Equations
- lctx.foldl f init start = (lctx.foldlM f init start).run
Equations
- lctx.foldr f init = (lctx.foldrM f init).run
Equations
- lctx.size = lctx.foldl (fun (n : Nat) (x : Lean.LocalDecl) => n + 1) 0
Equations
- lctx.findDecl? f = (lctx.findDeclM? f).run
Equations
- lctx.findDeclRev? f = (lctx.findDeclRevM? f).run
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
Equations
- One or more equations did not get rendered due to their size.
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
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
Return true
if lctx
contains a local declaration satisfying p
.
Equations
- lctx.any p = (lctx.anyM p).run
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.
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.
Sort the given FVarId
s by the order in which they appear in lctx
. If any of
the FVarId
s do not appear in lctx
, the result is unspecified.
Equations
- One or more equations did not get rendered due to their size.
Class used to denote that m
has a local context.
- getLCtx : m Lean.LocalContext
Return local hypotheses which are not "implementation detail", as Expr
s.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.