- default: Lean.LocalDeclKind
Participates fully in type class search, tactics, and is shown even if inaccessible.
For example: the
xinfun 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) + barexpands tofoo >>= fun __tmp => pure (__tmp + bar), where__tmphas theimplDetailkind. - 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 → Natto allow recursive calls. This declaration has theauxDeclkind.
Whether a local declaration should be found by type class search, tactics, etc. and shown in the goal display.
Instances For
- 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
A declaration for a LocalContext. This is used to register which free variables are in scope. Each declaration comes with
indexthe position of the decl in the local contextfvarIdthe unique id of the free variablesuserNamethe pretty-printable name of the variabletypethe type. Acdeclis a local variable, aldeclis a let-bound free variable with avalue : Expr.
Instances For
Instances For
Instances For
Instances For
Is the local declaration an implementation-detail hypothesis (including auxiliary declarations)?
Instances For
Instances For
- 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.
Instances For
Instances For
Instances For
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.
Instances For
Low level API for let declarations. Do not use directly.
Instances For
Low level API for adding a local declaration. Do not use directly.
Instances For
Instances For
Instances For
Instances For
Gets the declaration for expression e in the local context.
If e is not a free variable or not present then panics.
Instances For
Instances For
Returns true when the lctx contains the free variable e.
Panics if e is not an fvar.
Instances For
Return all of the free variables in the given context.
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
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.
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
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.
Instances For
Instances For
Creates the expression fun x₁ .. xₙ => b for free variables xs = #[x₁, .., xₙ],
suitably abstracting b and the types for each of the xᵢ.
Instances For
Creates the expression (x₁:α₁) → .. → (xₙ:αₙ) → b for free variables xs = #[x₁, .., xₙ],
suitably abstracting b and the types for each of the xᵢ, αᵢ.
Instances For
Instances For
Instances For
Return true if lctx contains a local declaration satisfying p.
Instances For
Return true if all declarations in lctx satisfy p.
Instances For
If option pp.sanitizeNames is set to true, add tombstone to shadowed local declaration names and ones contains macroscopes.