inductive Lean.Elab.Do.LetOrReassign : Type

• let (mutTk? : Option Syntax) (erased : Bool) : LetOrReassign
• have : LetOrReassign
• reassign : LetOrReassign

def Lean.Elab.Do.LetOrReassign.getLetMutTk? (letOrReassign : LetOrReassign) : Option Syntax

Equations

• (Lean.Elab.Do.LetOrReassign.let mutTk? erased).getLetMutTk? = mutTk?
• letOrReassign.getLetMutTk? = none

def Lean.Elab.Do.LetOrReassign.isErasedDecl (letOrReassign : LetOrReassign) : Bool

Equations

• (Lean.Elab.Do.LetOrReassign.let mutTk? erased).isErasedDecl = erased
• letOrReassign.isErasedDecl = false

def Lean.Elab.Do.isErased (letOrReassign : LetOrReassign) (vars : Array Ident) : DoElabM Bool

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Do.isErased (Lean.Elab.Do.LetOrReassign.let mutTk? erased) vars = pure erased
• Lean.Elab.Do.isErased letOrReassign vars = pure false

def Lean.Elab.Do.LetOrReassign.checkMutVars (letOrReassign : LetOrReassign) (vars : Array Ident) : DoElabM Unit

Equations

• One or more equations did not get rendered due to their size.
• letOrReassign.checkMutVars vars = Lean.Elab.Do.checkMutVarsForShadowing vars

def Lean.Elab.Do.LetOrReassign.registerReassignAliasInfo (letOrReassign : LetOrReassign) (vars : Array Ident) : DoElabM Unit

Equations

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

def Lean.Elab.Do.elabWithReassignments (letOrReassign : LetOrReassign) (vars : Array Ident) (k : DoElabM Expr) : DoElabM Expr

Equations

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

partial def Lean.Elab.Do.elabDoLetOrReassign (config : Term.LetConfig) (letOrReassign : LetOrReassign) (decl : TSyntax `Lean.Parser.Term.letDecl) (tk : Syntax) (dec : DoElemCont) : DoElabM Expr

def Lean.Elab.Do.elabDoLet : DoElab

Equations

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

def Lean.Elab.Do.elabDoErased : DoElab

Equations

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

def Lean.Elab.Do.expandDoErasedArrow : Macro

Equations

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

def Lean.Elab.Do.elabDoHave : DoElab

Equations

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

def Lean.Elab.Do.elabDoLetRec : DoElab

Equations

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

def Lean.Elab.Do.elabDoReassign : DoElab

Equations

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

def Lean.Elab.Do.elabDoLetElse : DoElab

Equations

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

def Lean.Elab.Do.elabDoLetArrow : DoElab

Equations

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

def Lean.Elab.Do.elabDoReassignArrow : DoElab

Equations

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