Lean.LocalContext

Type

cdecl: Nat → Lean.FVarId → Lean.Name → Lean.Expr → Lean.BinderInfo → Lean.LocalDecl
ldecl: Nat → Lean.FVarId → Lean.Name → Lean.Expr → Lean.Expr → Bool → 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.

source

instance Lean.instInhabitedLocalDecl:

Inhabited Lean.LocalDecl

Equations

Lean.instInhabitedLocalDecl = { default := Lean.LocalDecl.cdecl default default default default default }

source

@[export lean_mk_local_decl]

def Lean.mkLocalDeclEx (index : Nat) (fvarId : Lean.FVarId) (userName : Lean.Name) (type : Lean.Expr) (bi : Lean.BinderInfo) :

Lean.LocalDecl

Equations

Lean.mkLocalDeclEx index fvarId userName type bi = Lean.LocalDecl.cdecl index fvarId userName type bi

source

@[export lean_mk_let_decl]

def Lean.mkLetDeclEx (index : Nat) (fvarId : Lean.FVarId) (userName : Lean.Name) (type : Lean.Expr) (val : Lean.Expr) :

Lean.LocalDecl

Equations

Lean.mkLetDeclEx index fvarId userName type val = Lean.LocalDecl.ldecl index fvarId userName type val false

source

@[export lean_local_decl_binder_info]

def Lean.LocalDecl.binderInfoEx:

Lean.LocalDecl → Lean.BinderInfo

Equations

Lean.LocalDecl.binderInfoEx _fun_discr = match _fun_discr with | Lean.LocalDecl.cdecl index fvarId userName type bi => bi | x => Lean.BinderInfo.default

source

def Lean.LocalDecl.isLet:

Lean.LocalDecl → Bool

Equations

Lean.LocalDecl.isLet _fun_discr = match _fun_discr with | Lean.LocalDecl.cdecl index fvarId userName type bi => false | Lean.LocalDecl.ldecl index fvarId userName type value nonDep => true

source

def Lean.LocalDecl.index:

Lean.LocalDecl → Nat

Equations

Lean.LocalDecl.index _fun_discr = match _fun_discr with | Lean.LocalDecl.cdecl i fvarId userName type bi => i | Lean.LocalDecl.ldecl i fvarId userName type value nonDep => i

source

def Lean.LocalDecl.setIndex:

Lean.LocalDecl → Nat → Lean.LocalDecl

Equations

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

source

def Lean.LocalDecl.fvarId:

Lean.LocalDecl → Lean.FVarId

Equations

Lean.LocalDecl.fvarId _fun_discr = match _fun_discr with | Lean.LocalDecl.cdecl index id userName type bi => id | Lean.LocalDecl.ldecl index id userName type value nonDep => id

source

def Lean.LocalDecl.userName:

Lean.LocalDecl → Lean.Name

Equations

Lean.LocalDecl.userName _fun_discr = match _fun_discr with | Lean.LocalDecl.cdecl index fvarId n type bi => n | Lean.LocalDecl.ldecl index fvarId n type value nonDep => n

source

def Lean.LocalDecl.type:

Lean.LocalDecl → Lean.Expr

Equations

Lean.LocalDecl.type _fun_discr = match _fun_discr with | Lean.LocalDecl.cdecl index fvarId userName t bi => t | Lean.LocalDecl.ldecl index fvarId userName t value nonDep => t

source

def Lean.LocalDecl.setType:

Lean.LocalDecl → Lean.Expr → Lean.LocalDecl

Equations

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

source

def Lean.LocalDecl.binderInfo:

Lean.LocalDecl → Lean.BinderInfo

Equations

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

source

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

Bool

Equations

Lean.LocalDecl.isAuxDecl d = Lean.BinderInfo.isAuxDecl (Lean.LocalDecl.binderInfo d)

source

def Lean.LocalDecl.value?:

Lean.LocalDecl → Option Lean.Expr

Equations

Lean.LocalDecl.value? _fun_discr = match _fun_discr with | Lean.LocalDecl.cdecl index fvarId userName type bi => none | Lean.LocalDecl.ldecl index fvarId userName type v nonDep => some v

source

def Lean.LocalDecl.value:

Lean.LocalDecl → Lean.Expr

Equations

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

source

def Lean.LocalDecl.hasValue:

Lean.LocalDecl → Bool

Equations

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

source

def Lean.LocalDecl.setValue:

Lean.LocalDecl → Lean.Expr → Lean.LocalDecl

Equations

Lean.LocalDecl.setValue _fun_discr _fun_discr = match _fun_discr, _fun_discr with | Lean.LocalDecl.ldecl idx id n t value nd, v => Lean.LocalDecl.ldecl idx id n t v nd | d, x => d

source

def Lean.LocalDecl.setUserName:

Lean.LocalDecl → Lean.Name → Lean.LocalDecl

Equations

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

source

def Lean.LocalDecl.setBinderInfo:

Lean.LocalDecl → Lean.BinderInfo → Lean.LocalDecl

Equations

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

source

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

Lean.Expr

Equations

Lean.LocalDecl.toExpr decl = Lean.mkFVar (Lean.LocalDecl.fvarId decl)

source

def Lean.LocalDecl.hasExprMVar:

Lean.LocalDecl → Bool

Equations

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

source

structure Lean.LocalContext:

Type

fvarIdToDecl : Std.PersistentHashMap Lean.FVarId Lean.LocalDecl
decls : Std.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.

source

instance Lean.instInhabitedLocalContext:

Inhabited Lean.LocalContext

Equations

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

source

@[export lean_mk_empty_local_ctx]

def Lean.LocalContext.mkEmpty:

Unit → Lean.LocalContext

Equations

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

source

def Lean.LocalContext.empty:

Lean.LocalContext

Equations

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

source

@[export lean_local_ctx_is_empty]

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

Bool

Equations

Lean.LocalContext.isEmpty lctx = Std.PersistentHashMap.isEmpty lctx.fvarIdToDecl

source

@[export lean_local_ctx_mk_local_decl]

def Lean.LocalContext.mkLocalDecl (lctx : Lean.LocalContext) (fvarId : Lean.FVarId) (userName : Lean.Name) (type : Lean.Expr) (bi : optParam Lean.BinderInfo Lean.BinderInfo.default) :

Lean.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.

source

@[export lean_local_ctx_mk_let_decl]

def Lean.LocalContext.mkLetDecl (lctx : Lean.LocalContext) (fvarId : Lean.FVarId) (userName : Lean.Name) (type : Lean.Expr) (value : Lean.Expr) (nonDep : optParam Bool false) :

Lean.LocalContext

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

Equations

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

source

def Lean.LocalContext.addDecl (lctx : Lean.LocalContext) (newDecl : Lean.LocalDecl) :

Lean.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.

source

@[export lean_local_ctx_find]

def Lean.LocalContext.find? (lctx : Lean.LocalContext) (fvarId : Lean.FVarId) :

Option Lean.LocalDecl

Equations

Lean.LocalContext.find? lctx fvarId = Std.PersistentHashMap.find? lctx.fvarIdToDecl fvarId

source

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

Option Lean.LocalDecl

Equations

Lean.LocalContext.findFVar? lctx e = Lean.LocalContext.find? lctx (Lean.Expr.fvarId! e)

source

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

Lean.LocalDecl

Equations

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

source

def Lean.LocalContext.getFVar! (lctx : Lean.LocalContext) (e : Lean.Expr) :

Lean.LocalDecl

Gets the declaration for expression e in the local context. If e is not a free variable or not present then panics.

Equations

Lean.LocalContext.getFVar! lctx e = Lean.LocalContext.get! lctx (Lean.Expr.fvarId! e)

source

def Lean.LocalContext.contains (lctx : Lean.LocalContext) (fvarId : Lean.FVarId) :

Bool

Equations

Lean.LocalContext.contains lctx fvarId = Std.PersistentHashMap.contains lctx.fvarIdToDecl fvarId

source

def Lean.LocalContext.containsFVar (lctx : Lean.LocalContext) (e : Lean.Expr) :

Bool

Returns true when the lctx contains the free variable e. Panics if e is not an fvar.

Equations

Lean.LocalContext.containsFVar lctx e = Lean.LocalContext.contains lctx (Lean.Expr.fvarId! e)

source

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

Array Lean.FVarId

Equations

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

source

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

Array Lean.Expr

Return all of the free variables in the given context.

Equations

Lean.LocalContext.getFVars lctx = Array.map Lean.mkFVar (Lean.LocalContext.getFVarIds lctx)

source

@[export lean_local_ctx_erase]

def Lean.LocalContext.erase (lctx : Lean.LocalContext) (fvarId : Lean.FVarId) :

Lean.LocalContext

Equations

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

source

@[export lean_local_ctx_pop]

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

Lean.LocalContext

Equations

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

source

@[export lean_local_ctx_find_from_user_name]

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

Option Lean.LocalDecl

Equations

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

source

@[export lean_local_ctx_uses_user_name]

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

Bool

Equations

Lean.LocalContext.usesUserName lctx userName = Option.isSome (Lean.LocalContext.findFromUserName? lctx userName)

source

@[export lean_local_ctx_get_unused_name]

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

Lean.Name

Equations

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

source

@[export lean_local_ctx_last_decl]

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

Option Lean.LocalDecl

Equations

Lean.LocalContext.lastDecl lctx = Std.PersistentArray.get! lctx.decls (lctx.decls.size - 1)

source

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

Lean.LocalContext

Equations

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

source

@[export lean_local_ctx_rename_user_name]

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

Lean.LocalContext

Equations

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

source

@[inline]

def Lean.LocalContext.modifyLocalDecl (lctx : Lean.LocalContext) (fvarId : Lean.FVarId) (f : Lean.LocalDecl → Lean.LocalDecl) :

Lean.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.

source

def Lean.LocalContext.setBinderInfo (lctx : Lean.LocalContext) (fvarId : Lean.FVarId) (bi : Lean.BinderInfo) :

Lean.LocalContext

Equations

Lean.LocalContext.setBinderInfo lctx fvarId bi = Lean.LocalContext.modifyLocalDecl lctx fvarId fun decl => Lean.LocalDecl.setBinderInfo decl bi

source

@[export lean_local_ctx_num_indices]

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

Nat

Equations

Lean.LocalContext.numIndices lctx = lctx.decls.size

source

@[export lean_local_ctx_get]

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

Option Lean.LocalDecl

Equations

Lean.LocalContext.getAt? lctx i = Std.PersistentArray.get! lctx.decls i

source

@[specialize]

def Lean.LocalContext.foldlM {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] (lctx : Lean.LocalContext) (f : β → Lean.LocalDecl → m β) (init : β) (start : optParam Nat 0) :

m β

Equations

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

source

@[specialize]

def Lean.LocalContext.foldrM {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] (lctx : Lean.LocalContext) (f : Lean.LocalDecl → β → m β) (init : β) :

m β

Equations

Lean.LocalContext.foldrM lctx f init = Std.PersistentArray.foldrM lctx.decls (fun decl b => match decl with | none => pure b | some decl => f decl b) init

source

@[specialize]

def Lean.LocalContext.forM {m : Type u_1 → Type u_2} [inst : Monad m] (lctx : Lean.LocalContext) (f : Lean.LocalDecl → m PUnit) :

m PUnit

Equations

Lean.LocalContext.forM lctx f = Std.PersistentArray.forM lctx.decls fun decl => match decl with | none => pure PUnit.unit | some decl => f decl

source

@[specialize]

def Lean.LocalContext.findDeclM? {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] (lctx : Lean.LocalContext) (f : Lean.LocalDecl → m (Option β)) :

m (Option β)

Equations

Lean.LocalContext.findDeclM? lctx f = Std.PersistentArray.findSomeM? lctx.decls fun decl => match decl with | none => pure none | some decl => f decl

source

@[specialize]

def Lean.LocalContext.findDeclRevM? {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] (lctx : Lean.LocalContext) (f : Lean.LocalDecl → m (Option β)) :

m (Option β)

Equations

Lean.LocalContext.findDeclRevM? lctx f = Std.PersistentArray.findSomeRevM? lctx.decls fun decl => match decl with | none => pure none | some decl => f decl

source

instance Lean.LocalContext.instForInLocalContextLocalDecl {m : Type u_1 → Type u_2} :

ForIn m Lean.LocalContext Lean.LocalDecl

Equations

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

source

@[inline]

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

Equations

Lean.LocalContext.foldl lctx f init start = Id.run (Lean.LocalContext.foldlM lctx f init start)

source

@[inline]

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

Equations

Lean.LocalContext.foldr lctx f init = Id.run (Lean.LocalContext.foldrM lctx f init)

source

@[inline]

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

Option β

Equations

Lean.LocalContext.findDecl? lctx f = Id.run (Lean.LocalContext.findDeclM? lctx f)

source

@[inline]

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

Option β

Equations

Lean.LocalContext.findDeclRev? lctx f = Id.run (Lean.LocalContext.findDeclRevM? lctx f)

source

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

Bool

source

def Lean.LocalContext.isSubPrefixOf (lctx₁ : Lean.LocalContext) (lctx₂ : Lean.LocalContext) (exceptFVars : optParam (Array Lean.Expr) #[]) :

Bool

Equations

Lean.LocalContext.isSubPrefixOf lctx₁ lctx₂ exceptFVars = Lean.LocalContext.isSubPrefixOfAux lctx₁.decls lctx₂.decls exceptFVars 0 0

source

@[inline]

def Lean.LocalContext.mkBinding (isLambda : Bool) (lctx : Lean.LocalContext) (xs : Array Lean.Expr) (b : Lean.Expr) :

Lean.Expr

Equations

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

source

def Lean.LocalContext.mkLambda (lctx : Lean.LocalContext) (xs : Array Lean.Expr) (b : Lean.Expr) :

Lean.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

Lean.LocalContext.mkLambda lctx xs b = Lean.LocalContext.mkBinding true lctx xs b

source

def Lean.LocalContext.mkForall (lctx : Lean.LocalContext) (xs : Array Lean.Expr) (b : Lean.Expr) :

Lean.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