Documentation

Lean.LocalContext

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 : NatNat to allow recursive calls. This declaration has the auxDecl kind.

Instances For
Equations
inductive Lean.LocalDecl :

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.
Instances For
Equations
@[export lean_mk_local_decl]
def Lean.mkLocalDeclEx (index : Nat) (fvarId : Lean.FVarId) (userName : Lean.Name) (type : Lean.Expr) (bi : Lean.BinderInfo) :
Equations
@[export lean_mk_let_decl]
def Lean.mkLetDeclEx (index : Nat) (fvarId : Lean.FVarId) (userName : Lean.Name) (type val : Lean.Expr) :
Equations
@[export lean_local_decl_binder_info]
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations

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

Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations

Set the kind of a LocalDecl.

Equations

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
Equations
@[export lean_mk_empty_local_ctx]
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.
@[export lean_local_ctx_is_empty]
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.
def Lean.LocalContext.mkLetDecl (lctx : Lean.LocalContext) (fvarId : Lean.FVarId) (userName : Lean.Name) (type value : Lean.Expr) (nonDep : Bool := false) (kind : Lean.LocalDeclKind := default) :

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.
@[export lean_local_ctx_find]
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

Return all of the free variables in the given context.

Equations
@[export lean_local_ctx_erase]
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
  • lctx.lastDecl = lctx.decls.get! (lctx.decls.size - 1)
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.
@[inline]

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
@[export lean_local_ctx_num_indices]
Equations
  • lctx.numIndices = lctx.decls.size
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.LocalDeclm β) (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 : 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.LocalDeclm PUnit) :
Equations
@[specialize #[]]
def Lean.LocalContext.findDeclM? {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (lctx : Lean.LocalContext) (f : Lean.LocalDeclm (Option β)) :
m (Option β)
Equations
@[specialize #[]]
def Lean.LocalContext.findDeclRevM? {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (lctx : Lean.LocalContext) (f : Lean.LocalDeclm (Option β)) :
m (Option β)
Equations
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 : 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
Equations
@[inline]
Equations
  • lctx.findDecl? f = (lctx.findDeclM? f).run
@[inline]
Equations
  • lctx.findDeclRev? f = (lctx.findDeclRevM? f).run
def Lean.LocalContext.isSubPrefixOf (lctx₁ lctx₂ : Lean.LocalContext) (exceptFVars : Array Lean.Expr := #[]) :

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

Creates the expression (x₁:α₁) → .. → (xₙ:αₙ) → b for free variables xs = #[x₁, .., xₙ], suitably abstracting b and the types for each of the xᵢ, αᵢ.

Equations
@[inline]
def Lean.LocalContext.anyM {m : TypeType u_1} [Monad m] (lctx : Lean.LocalContext) (p : Lean.LocalDeclm Bool) :
Equations
@[inline]
def Lean.LocalContext.allM {m : TypeType u_1} [Monad m] (lctx : Lean.LocalContext) (p : Lean.LocalDeclm Bool) :
Equations
@[inline]

Return true if lctx contains a local declaration satisfying p.

Equations
  • lctx.any p = (lctx.anyM p).run
@[inline]

Return true if all declarations in lctx satisfy p.

Equations
  • lctx.all p = (lctx.allM 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 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 : TypeType) :

Class used to denote that m has a local context.

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

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

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.