inductive Lean.LocalDeclKind : Type

Whether a local declaration should be found by type class search, tactics, etc. and shown in the goal display.

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

Instances For

• Lean.instHashableLocalDeclKind
• Lean.instInhabitedLocalDeclKind
• Lean.instReprLocalDeclKind

instance Lean.instInhabitedLocalDeclKind : Inhabited LocalDeclKind

Equations

• Lean.instInhabitedLocalDeclKind = { default := Lean.LocalDeclKind.default }

instance Lean.instReprLocalDeclKind : Repr LocalDeclKind

Equations

• Lean.instReprLocalDeclKind = { reprPrec := Lean.reprLocalDeclKind✝ }

instance Lean.instDecidableEqLocalDeclKind : DecidableEq LocalDeclKind

Equations

• Lean.instDecidableEqLocalDeclKind x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance Lean.instHashableLocalDeclKind : Hashable LocalDeclKind

Equations

• Lean.instHashableLocalDeclKind = { hash := Lean.hashLocalDeclKind✝ }

inductive Lean.LocalDecl : Type

A declaration for a LocalContext. This is used to register which free variables are in scope.

See LocalDecl.index, LocalDecl.fvarId, LocalDecl.userName, LocalDecl.type for accessors for arguments common to both constructors.

• cdecl (index : Nat) (fvarId : FVarId) (userName : Name) (type : Expr) (bi : BinderInfo) (kind : LocalDeclKind) : LocalDecl

  A local variable.

• ldecl (index : Nat) (fvarId : FVarId) (userName : Name) (type value : Expr) (nonDep : Bool) (kind : LocalDeclKind) : LocalDecl

  A let-bound free variable, with a value : Expr.

Instances For

• Lean.LocalContext.instForInLocalDecl
• Lean.instInhabitedLocalDecl

instance Lean.instInhabitedLocalDecl : Inhabited LocalDecl

Equations

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

@[export lean_mk_local_decl]

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

Equations

• Lean.mkLocalDeclEx index fvarId userName type bi = Lean.LocalDecl.cdecl index fvarId userName type bi Lean.LocalDeclKind.default

@[export lean_mk_let_decl]

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

Equations

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

@[export lean_local_decl_binder_info]

def Lean.LocalDecl.binderInfoEx : LocalDecl → BinderInfo

Equations

• (Lean.LocalDecl.cdecl index fvarId userName type bi kind).binderInfoEx = bi
• x✝.binderInfoEx = Lean.BinderInfo.default

def Lean.LocalDecl.isLet : LocalDecl → Bool

Equations

• (Lean.LocalDecl.cdecl index fvarId userName type bi kind).isLet = false
• (Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind).isLet = true

def Lean.LocalDecl.index : LocalDecl → Nat

The position of the decl in the local context.

Equations

• (Lean.LocalDecl.cdecl index fvarId userName type bi kind).index = index
• (Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind).index = index

def Lean.LocalDecl.setIndex : LocalDecl → Nat → LocalDecl

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

def Lean.LocalDecl.fvarId : LocalDecl → FVarId

The unique id of the free variable.

Equations

• (Lean.LocalDecl.cdecl index fvarId userName type bi kind).fvarId = fvarId
• (Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind).fvarId = fvarId

def Lean.LocalDecl.userName : LocalDecl → Name

The pretty-printable name of the variable.

Equations

• (Lean.LocalDecl.cdecl index fvarId userName type bi kind).userName = userName
• (Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind).userName = userName

def Lean.LocalDecl.type : LocalDecl → Expr

The type of the variable.

Equations

• (Lean.LocalDecl.cdecl index fvarId userName type bi kind).type = type
• (Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind).type = type

def Lean.LocalDecl.setType : LocalDecl → Expr → LocalDecl

Equations

• (Lean.LocalDecl.cdecl idx id n type bi k).setType x✝ = Lean.LocalDecl.cdecl idx id n x✝ bi k
• (Lean.LocalDecl.ldecl idx id n type v nd k).setType x✝ = Lean.LocalDecl.ldecl idx id n x✝ v nd k

def Lean.LocalDecl.binderInfo : LocalDecl → BinderInfo

Equations

• (Lean.LocalDecl.cdecl index fvarId userName type bi kind).binderInfo = bi
• (Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind).binderInfo = Lean.BinderInfo.default

def Lean.LocalDecl.kind : LocalDecl → LocalDeclKind

Equations

• (Lean.LocalDecl.cdecl index fvarId userName type bi kind).kind = kind
• (Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind).kind = kind

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

Equations

• d.isAuxDecl = decide (d.kind = Lean.LocalDeclKind.auxDecl)

def Lean.LocalDecl.isImplementationDetail (d : LocalDecl) : Bool

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

Equations

• d.isImplementationDetail = (d.kind != Lean.LocalDeclKind.default)

def Lean.LocalDecl.value? : LocalDecl → Option Expr

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

def Lean.LocalDecl.value : LocalDecl → Expr

Equations

• (Lean.LocalDecl.cdecl index fvarId userName type bi kind).value = panicWithPosWithDecl "Lean.LocalContext" "Lean.LocalDecl.value" 123 29 "let declaration expected"
• (Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind).value = value

def Lean.LocalDecl.hasValue : LocalDecl → Bool

Equations

• (Lean.LocalDecl.cdecl index fvarId userName type bi kind).hasValue = false
• (Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind).hasValue = true

def Lean.LocalDecl.setValue : LocalDecl → Expr → LocalDecl

Equations

• (Lean.LocalDecl.ldecl idx id n t value nd k).setValue x✝ = Lean.LocalDecl.ldecl idx id n t x✝ nd k
• x✝¹.setValue x✝ = x✝¹

def Lean.LocalDecl.setUserName : LocalDecl → Name → LocalDecl

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

def Lean.LocalDecl.setBinderInfo : LocalDecl → BinderInfo → LocalDecl

Equations

• (Lean.LocalDecl.cdecl index id n type bi k).setBinderInfo x✝ = Lean.LocalDecl.cdecl index id n type x✝ k
• (Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind).setBinderInfo x✝ = panicWithPosWithDecl "Lean.LocalContext" "Lean.LocalDecl.setBinderInfo" 140 38 "unexpected let declaration"

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

Equations

• decl.toExpr = Lean.mkFVar decl.fvarId

def Lean.LocalDecl.hasExprMVar : LocalDecl → Bool

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)

def Lean.LocalDecl.setKind : LocalDecl → LocalDeclKind → LocalDecl

Set the kind of a LocalDecl.

Equations

• (Lean.LocalDecl.cdecl index fvarId userName type bi kind).setKind x✝ = Lean.LocalDecl.cdecl index fvarId userName type bi x✝
• (Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind).setKind x✝ = Lean.LocalDecl.ldecl index fvarId userName type value nonDep x✝

structure Lean.LocalContext : Type

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 : PersistentHashMap FVarId LocalDecl
• decls : PersistentArray (Option LocalDecl)

Instances For

• Lean.LocalContext.instForInLocalDecl
• Lean.Widget.instTypeNameLocalContext
• Lean.instInhabitedLocalContext

instance Lean.instInhabitedLocalContext : Inhabited LocalContext

Equations

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

@[export lean_mk_empty_local_ctx]

def Lean.LocalContext.mkEmpty : Unit → LocalContext

Equations

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

def Lean.LocalContext.empty : LocalContext

Equations

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

@[export lean_local_ctx_is_empty]

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

Equations

• lctx.isEmpty = lctx.fvarIdToDecl.isEmpty

def Lean.LocalContext.mkLocalDecl (lctx : LocalContext) (fvarId : FVarId) (userName : Name) (type : Expr) (bi : BinderInfo := BinderInfo.default) (kind : LocalDeclKind := LocalDeclKind.default) : 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.

def Lean.LocalContext.mkLetDecl (lctx : LocalContext) (fvarId : FVarId) (userName : Name) (type value : Expr) (nonDep : Bool := false) (kind : LocalDeclKind := default) : LocalContext

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

Equations

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

def Lean.LocalContext.addDecl (lctx : LocalContext) (newDecl : LocalDecl) : 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.

@[export lean_local_ctx_find]

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

Equations

• lctx.find? fvarId = lctx.fvarIdToDecl.find? fvarId

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

Equations

• lctx.findFVar? e = lctx.find? e.fvarId!

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

Equations

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

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

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!

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

Equations

• lctx.contains fvarId = lctx.fvarIdToDecl.contains fvarId

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

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!

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

Equations

• lctx.getFVarIds = lctx.decls.foldl (fun (r : Array Lean.FVarId) (decl? : Option Lean.LocalDecl) => match decl? with | some decl => r.push decl.fvarId | none => r) #[]

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

Return all of the free variables in the given context.

Equations

• lctx.getFVars = Array.map Lean.mkFVar lctx.getFVarIds

@[export lean_local_ctx_erase]

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• lctx.usesUserName userName = (lctx.findFromUserName? userName).isSome

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

Equations

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

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

Equations

• lctx.lastDecl = lctx.decls[lctx.decls.size - 1]!

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

Equations

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

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

Equations

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

@[inline]

def Lean.LocalContext.modifyLocalDecl (lctx : LocalContext) (fvarId : FVarId) (f : LocalDecl → LocalDecl) : 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.

def Lean.LocalContext.setKind (lctx : LocalContext) (fvarId : FVarId) (kind : LocalDeclKind) : LocalContext

Set the kind of the given fvar.

Equations

• lctx.setKind fvarId kind = lctx.modifyLocalDecl fvarId fun (x : Lean.LocalDecl) => x.setKind kind

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

Equations

• lctx.setBinderInfo fvarId bi = lctx.modifyLocalDecl fvarId fun (decl : Lean.LocalDecl) => decl.setBinderInfo bi

@[export lean_local_ctx_num_indices]

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

Equations

• lctx.numIndices = lctx.decls.size

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

Equations

• lctx.getAt? i = lctx.decls[i]!

@[specialize #[]]

def Lean.LocalContext.foldlM {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (lctx : LocalContext) (f : β → LocalDecl → m β) (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 : LocalContext) (f : 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 : LocalContext) (f : LocalDecl → m PUnit) : m PUnit

Equations

• lctx.forM f = lctx.decls.forM fun (decl : Option Lean.LocalDecl) => match decl with | none => pure PUnit.unit | some decl => f decl

@[specialize #[]]

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

Equations

• lctx.findDeclM? f = lctx.decls.findSomeM? fun (decl : Option Lean.LocalDecl) => match decl with | none => pure none | some decl => f decl

@[specialize #[]]

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

Equations

• lctx.findDeclRevM? f = lctx.decls.findSomeRevM? fun (decl : Option Lean.LocalDecl) => match decl with | none => pure none | some decl => f decl

instance Lean.LocalContext.instForInLocalDecl {m : Type u_1 → Type u_2} : ForIn m LocalContext LocalDecl

Equations

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

@[inline]

def Lean.LocalContext.foldl {β : Type u_1} (lctx : LocalContext) (f : β → 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 : LocalContext) (f : LocalDecl → β → β) (init : β) : β

Equations

• lctx.foldr f init = (lctx.foldrM f init).run

def Lean.LocalContext.size (lctx : LocalContext) : Nat

Equations

• lctx.size = lctx.foldl (fun (n : Nat) (x : Lean.LocalDecl) => n + 1) 0

@[inline]

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

Equations

• lctx.findDecl? f = (lctx.findDeclM? f).run

@[inline]

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

Equations

• lctx.findDeclRev? f = (lctx.findDeclRevM? f).run

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

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

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

@[inline]

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

Equations

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

def Lean.LocalContext.mkLambda (lctx : LocalContext) (xs : Array Expr) (b : Expr) : 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

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

def Lean.LocalContext.mkForall (lctx : LocalContext) (xs : Array Expr) (b : Expr) : 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

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

@[inline]

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

Equations

• lctx.anyM p = lctx.decls.anyM fun (d : Option Lean.LocalDecl) => match d with | some decl => p decl | none => pure false

@[inline]

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

Equations

• lctx.allM p = lctx.decls.allM fun (d : Option Lean.LocalDecl) => match d with | some decl => p decl | none => pure true

@[inline]

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

Return true if lctx contains a local declaration satisfying p.

Equations

• lctx.any p = (lctx.anyM p).run

@[inline]

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

Return true if all declarations in lctx satisfy p.

Equations

• lctx.all p = (lctx.allM p).run

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

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.

def Lean.LocalContext.getRoundtrippingUserName? (lctx : LocalContext) (fvarId : FVarId) : Option Name

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.

def Lean.LocalContext.sortFVarsByContextOrder (lctx : LocalContext) (hyps : Array FVarId) : Array FVarId

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 : Type → Type) : Type

Class used to denote that m has a local context.

• getLCtx : m LocalContext

Instances

• Lean.Meta.instMonadLCtxMetaM
• Lean.instMonadLCtxOfMonadLift

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

Equations

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

def Lean.getLocalHyps {m : Type → Type} [Monad m] [MonadLCtx m] : m (Array Expr)

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

Equations

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

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

Equations

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

def Lean.LocalContext.replaceFVarId (fvarId : FVarId) (e : Expr) (lctx : LocalContext) : LocalContext

Equations

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