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.instReprLocalDeclKind = { reprPrec := Lean.reprLocalDeclKind✝ }
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.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).kind = kind
- (Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind).kind = kind
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 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
- 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
.
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
- 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.
Low level API for adding a local declaration. Do not use directly.
Equations
- lctx.findFVar? e = lctx.find? e.fvarId!
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.
Return all of the free variables in the given context.
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.
Set the kind of the given fvar.
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
- One or more equations did not get rendered due to their size.
Equations
- lctx.foldl f init start = (lctx.foldlM f init start).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
Return true
if all declarations in lctx
satisfy p
.
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.
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.
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.