Lean.LocalContext

source

inductive Lean.LocalDecl :

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

source

instance Lean.instInhabitedLocalDecl :

Inhabited Lean.LocalDecl

Equations

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

source

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

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

def Lean.LocalDecl.binderInfoEx :

Lean.LocalDecl → Lean.BinderInfo

Equations

Lean.LocalDecl.binderInfoEx x = match x with | Lean.LocalDecl.cdecl x x_1 x_2 x_3 bi => bi | x => Lean.BinderInfo.default

source

def Lean.LocalDecl.isLet :

Lean.LocalDecl → Bool

Equations

Lean.LocalDecl.isLet x = match x with | Lean.LocalDecl.cdecl x x_1 x_2 x_3 x_4 => false | Lean.LocalDecl.ldecl x x_1 x_2 x_3 x_4 x_5 => true

source

def Lean.LocalDecl.index :

Lean.LocalDecl → Nat

Equations

Lean.LocalDecl.index x = match x with | Lean.LocalDecl.cdecl i x x_1 x_2 x_3 => i | Lean.LocalDecl.ldecl i x x_1 x_2 x_3 x_4 => i

source

def Lean.LocalDecl.setIndex :

Lean.LocalDecl → Nat → Lean.LocalDecl

Equations

Lean.LocalDecl.setIndex x x = match x, x with | Lean.LocalDecl.cdecl x id n t bi, idx => Lean.LocalDecl.cdecl idx id n t bi | Lean.LocalDecl.ldecl x id n t v nd, idx => Lean.LocalDecl.ldecl idx id n t v nd

source

def Lean.LocalDecl.fvarId :

Lean.LocalDecl → Lean.FVarId

Equations

Lean.LocalDecl.fvarId x = match x with | Lean.LocalDecl.cdecl x id x_1 x_2 x_3 => id | Lean.LocalDecl.ldecl x id x_1 x_2 x_3 x_4 => id

source

def Lean.LocalDecl.userName :

Lean.LocalDecl → Lean.Name

Equations

Lean.LocalDecl.userName x = match x with | Lean.LocalDecl.cdecl x x_1 n x_2 x_3 => n | Lean.LocalDecl.ldecl x x_1 n x_2 x_3 x_4 => n

source

def Lean.LocalDecl.type :

Lean.LocalDecl → Lean.Expr

Equations

Lean.LocalDecl.type x = match x with | Lean.LocalDecl.cdecl x x_1 x_2 t x_3 => t | Lean.LocalDecl.ldecl x x_1 x_2 t x_3 x_4 => t

source

def Lean.LocalDecl.setType :

Lean.LocalDecl → Lean.Expr → Lean.LocalDecl

Equations

Lean.LocalDecl.setType x x = match x, x with | Lean.LocalDecl.cdecl idx id n x bi, t => Lean.LocalDecl.cdecl idx id n t bi | Lean.LocalDecl.ldecl idx id n x v nd, t => Lean.LocalDecl.ldecl idx id n t v nd

source

def Lean.LocalDecl.binderInfo :

Lean.LocalDecl → Lean.BinderInfo

Equations

Lean.LocalDecl.binderInfo x = match x with | Lean.LocalDecl.cdecl x x_1 x_2 x_3 bi => bi | Lean.LocalDecl.ldecl x x_1 x_2 x_3 x_4 x_5 => Lean.BinderInfo.default

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? x = match x with | Lean.LocalDecl.cdecl x x_1 x_2 x_3 x_4 => none | Lean.LocalDecl.ldecl x x_1 x_2 x_3 v x_4 => some v

source

def Lean.LocalDecl.value :

Lean.LocalDecl → Lean.Expr

Equations

Lean.LocalDecl.value x = match x with | Lean.LocalDecl.cdecl x x_1 x_2 x_3 x_4 => panicWithPosWithDecl "Lean.LocalContext" "Lean.LocalDecl.value" 69 29 "let declaration expected" | Lean.LocalDecl.ldecl x x_1 x_2 x_3 v x_4 => v

source

def Lean.LocalDecl.hasValue :

Lean.LocalDecl → Bool

Equations

Lean.LocalDecl.hasValue x = match x with | Lean.LocalDecl.cdecl x x_1 x_2 x_3 x_4 => false | Lean.LocalDecl.ldecl x x_1 x_2 x_3 x_4 x_5 => true

source

def Lean.LocalDecl.setValue :

Lean.LocalDecl → Lean.Expr → Lean.LocalDecl

Equations

Lean.LocalDecl.setValue x x = match x, x with | Lean.LocalDecl.ldecl idx id n t x 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

Lean.LocalDecl.setUserName x x = match x, x with | Lean.LocalDecl.cdecl index id x type bi, userName => Lean.LocalDecl.cdecl index id userName type bi | Lean.LocalDecl.ldecl index id x type val nd, userName => Lean.LocalDecl.ldecl index id userName type val nd

source

def Lean.LocalDecl.setBinderInfo :

Lean.LocalDecl → Lean.BinderInfo → Lean.LocalDecl

Equations

Lean.LocalDecl.setBinderInfo x x = match x, x with | Lean.LocalDecl.cdecl index id n type x, bi => Lean.LocalDecl.cdecl index id n type bi | Lean.LocalDecl.ldecl x x_1 x_2 x_3 x_4 x_5, x_6 => panicWithPosWithDecl "Lean.LocalContext" "Lean.LocalDecl.setBinderInfo" 86 36 "unexpected let declaration"

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

Lean.LocalDecl.hasExprMVar x = match x with | Lean.LocalDecl.cdecl x x_1 x_2 t x_3 => Lean.Expr.hasExprMVar t | Lean.LocalDecl.ldecl x x_1 x_2 t v x_3 => Lean.Expr.hasExprMVar t || Lean.Expr.hasExprMVar v

source

structure Lean.LocalContext :

Type

fvarIdToDecl : Std.PersistentHashMap Lean.FVarId Lean.LocalDecl
decls : Std.PersistentArray (Option Lean.LocalDecl)

source

instance Lean.instInhabitedLocalContext :

Inhabited Lean.LocalContext

Equations

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

source

def Lean.LocalContext.mkEmpty :

Unit → Lean.LocalContext

Equations

Lean.LocalContext.mkEmpty x = { fvarIdToDecl := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } }

source

def Lean.LocalContext.empty :

Lean.LocalContext

Equations

Lean.LocalContext.empty = { fvarIdToDecl := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } }

source

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

Bool

Equations

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

source

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

Equations

Lean.LocalContext.mkLocalDecl lctx fvarId userName type bi = match lctx with | { fvarIdToDecl := map, decls := decls } => let idx := decls.size; let decl := Lean.LocalDecl.cdecl idx fvarId userName type bi; { fvarIdToDecl := Std.PersistentHashMap.insert map fvarId decl, decls := Std.PersistentArray.push decls (some decl) }

source

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

Equations

Lean.LocalContext.mkLetDecl lctx fvarId userName type value nonDep = match lctx with | { fvarIdToDecl := map, decls := decls } => let idx := decls.size; let decl := Lean.LocalDecl.ldecl idx fvarId userName type value nonDep; { fvarIdToDecl := Std.PersistentHashMap.insert map fvarId decl, decls := Std.PersistentArray.push decls (some decl) }

source

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

Lean.LocalContext

Equations

Lean.LocalContext.addDecl lctx newDecl = match lctx with | { fvarIdToDecl := map, decls := decls } => let idx := decls.size; let newDecl := Lean.LocalDecl.setIndex newDecl idx; { fvarIdToDecl := Std.PersistentHashMap.insert map (Lean.LocalDecl.fvarId newDecl) newDecl, decls := Std.PersistentArray.push decls (some newDecl) }

source

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

Lean.LocalContext.get! lctx fvarId = match Lean.LocalContext.find? lctx fvarId with | some d => d | none => panicWithPosWithDecl "Lean.LocalContext" "Lean.LocalContext.get!" 150 14 "unknown free variable"

source

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

Lean.LocalDecl

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

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

Lean.LocalContext.getFVarIds lctx = Std.PersistentArray.foldl lctx.decls (fun r decl? => match decl? with | some decl => Array.push r (Lean.LocalDecl.fvarId decl) | none => r) #[]

source

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

Array Lean.Expr

Equations

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

source

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

Lean.LocalContext

Equations

Lean.LocalContext.erase lctx fvarId = match lctx with | { fvarIdToDecl := map, decls := decls } => match Std.PersistentHashMap.find? map fvarId with | none => lctx | some decl => { fvarIdToDecl := Std.PersistentHashMap.erase map fvarId, decls := Lean.LocalContext.popTailNoneAux (Std.PersistentArray.set decls (Lean.LocalDecl.index decl) none) }

source

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

Lean.LocalContext

Equations

Lean.LocalContext.pop lctx = match lctx with | { fvarIdToDecl := map, decls := decls } => if (decls.size == 0) = true then lctx else match Std.PersistentArray.get! decls (decls.size - 1) with | none => lctx | some decl => { fvarIdToDecl := Std.PersistentHashMap.erase map (Lean.LocalDecl.fvarId decl), decls := Lean.LocalContext.popTailNoneAux (Std.PersistentArray.pop decls) }

source

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

Option Lean.LocalDecl

Equations

Lean.LocalContext.findFromUserName? lctx userName = Std.PersistentArray.findSomeRev? lctx.decls fun decl => match decl with | none => none | some decl => if (Lean.LocalDecl.userName decl == userName) = true then some decl else none

source

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

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

Lean.Name

Equations

Lean.LocalContext.getUnusedName lctx suggestion = let suggestion := Lean.Name.eraseMacroScopes suggestion; if Lean.LocalContext.usesUserName lctx suggestion = true then (Lean.LocalContext.getUnusedNameAux lctx suggestion 1).fst else suggestion

source

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

Lean.LocalContext.setUserName lctx fvarId userName = let decl := Lean.LocalContext.get! lctx fvarId; let decl := Lean.LocalDecl.setUserName decl userName; { fvarIdToDecl := Std.PersistentHashMap.insert lctx.fvarIdToDecl (Lean.LocalDecl.fvarId decl) decl, decls := Std.PersistentArray.set lctx.decls (Lean.LocalDecl.index decl) (some decl) }

source

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

Lean.LocalContext

Equations

Lean.LocalContext.renameUserName lctx fromName toName = match lctx with | { fvarIdToDecl := map, decls := decls } => match Lean.LocalContext.findFromUserName? lctx fromName with | none => lctx | some decl => let decl := Lean.LocalDecl.setUserName decl toName; { fvarIdToDecl := Std.PersistentHashMap.insert map (Lean.LocalDecl.fvarId decl) decl, decls := Std.PersistentArray.set decls (Lean.LocalDecl.index decl) (some decl) }

source

@[inline]

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

Lean.LocalContext

Equations

Lean.LocalContext.modifyLocalDecl lctx fvarId f = match lctx with | { fvarIdToDecl := map, decls := decls } => match Lean.LocalContext.find? lctx fvarId with | none => lctx | some decl => let decl := f decl; { fvarIdToDecl := Std.PersistentHashMap.insert map (Lean.LocalDecl.fvarId decl) decl, decls := Std.PersistentArray.set decls (Lean.LocalDecl.index decl) (some decl) }

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

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

Nat

Equations

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

source

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

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

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

Lean.LocalContext.instForInLocalContextLocalDecl = { forIn := fun {β} [Monad m] lctx init f => Std.PersistentArray.forIn lctx.decls init fun d? b => match d? with | none => pure (ForInStep.yield b) | some d => f d b }

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

Lean.LocalContext.mkBinding isLambda lctx xs b = let b := Lean.Expr.abstract b xs; Nat.foldRev (fun i b => let x := Array.getOp xs i; match Lean.LocalContext.findFVar? lctx x with | some (Lean.LocalDecl.cdecl x x_1 n ty bi) => let ty := Lean.Expr.abstractRange ty i xs; if isLambda = true then Lean.mkLambda n bi ty b else Lean.mkForall n bi ty b | some (Lean.LocalDecl.ldecl x x_1 n ty val nonDep) => if Lean.Expr.hasLooseBVar b 0 = true then let ty := Lean.Expr.abstractRange ty i xs; let val := Lean.Expr.abstractRange val i xs; Lean.mkLet n ty val b nonDep else Lean.Expr.lowerLooseBVars b 1 1 | none => panicWithPosWithDecl "Lean.LocalContext" "Lean.LocalContext.mkBinding" 340 14 "unknown free variable") (Array.size xs) b

source

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

Lean.Expr

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

Equations

Lean.LocalContext.mkForall lctx xs b = Lean.LocalContext.mkBinding false lctx xs b

source

@[inline]

def Lean.LocalContext.anyM {m : Type → Type u_1} [inst : Monad m] (lctx : Lean.LocalContext) (p : Lean.LocalDecl → m Bool) :

m Bool

Equations

Lean.LocalContext.anyM lctx p = Std.PersistentArray.anyM lctx.decls fun d => match d with | some decl => p decl | none => pure false

source

@[inline]

def Lean.LocalContext.allM {m : Type → Type u_1} [inst : Monad m] (lctx : Lean.LocalContext) (p : Lean.LocalDecl → m Bool) :

m Bool

Equations

Lean.LocalContext.allM lctx p = Std.PersistentArray.allM lctx.decls fun d => match d with | some decl => p decl | none => pure true

source

@[inline]

def Lean.LocalContext.any (lctx : Lean.LocalContext) (p : Lean.LocalDecl → Bool) :

Bool

Equations

Lean.LocalContext.any lctx p = Id.run (Lean.LocalContext.anyM lctx p)

source

@[inline]

def Lean.LocalContext.all (lctx : Lean.LocalContext) (p : Lean.LocalDecl → Bool) :

Bool

Equations

Lean.LocalContext.all lctx p = Id.run (Lean.LocalContext.allM lctx p)

source

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

StateM Lean.NameSanitizerState Lean.LocalContext

Equations

Lean.LocalContext.sanitizeNames lctx = do let st ← get if (!Lean.getSanitizeNames st.options) = true then pure lctx else StateT.run' (Nat.foldRevM (fun i lctx => match Std.PersistentArray.getOp lctx.decls i with | none => pure lctx | some decl => do let a ← get if (Lean.Name.hasMacroScopes (Lean.LocalDecl.userName decl) || Lean.NameSet.contains a (Lean.LocalDecl.userName decl)) = true then do modify fun s => Lean.NameSet.insert s (Lean.LocalDecl.userName decl) let userNameNew ← liftM (Lean.sanitizeName (Lean.LocalDecl.userName decl)) pure (Lean.LocalContext.setUserName lctx (Lean.LocalDecl.fvarId decl) userNameNew) else do modify fun s => Lean.NameSet.insert s (Lean.LocalDecl.userName decl) pure lctx) lctx lctx.decls.size) ∅

source

class Lean.MonadLCtx (m : Type → Type) :

Type

getLCtx : m Lean.LocalContext

Instances

source

instance Lean.instMonadLCtx {m : Type → Type} {n : Type → Type} [inst : MonadLift m n] [inst : Lean.MonadLCtx m] :

Lean.MonadLCtx n

Equations

Lean.instMonadLCtx = { getLCtx := liftM Lean.getLCtx }

source

def Lean.replaceFVarIdAtLocalDecl (fvarId : Lean.FVarId) (e : Lean.Expr) (d : Lean.LocalDecl) :

Lean.LocalDecl

Equations

Lean.replaceFVarIdAtLocalDecl fvarId e d = if (Lean.LocalDecl.fvarId d == fvarId) = true then d else match d with | Lean.LocalDecl.cdecl idx id n type bi => Lean.LocalDecl.cdecl idx id n (Lean.Expr.replaceFVarId type fvarId e) bi | Lean.LocalDecl.ldecl idx id n type val nonDep => Lean.LocalDecl.ldecl idx id n (Lean.Expr.replaceFVarId type fvarId e) (Lean.Expr.replaceFVarId val fvarId e) nonDep