inductive Lean.Elab.Do.LetOrReassign : Type

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

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

Equations

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

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

Equations

• Lean.Elab.Do.LetOrReassign.reassign.checkMutVars vars = Lean.Elab.Do.throwUnlessMutVarsDeclared vars
• 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.elabDoLetOrReassignWith (hint : MessageData) (letOrReassign : LetOrReassign) (vars : Array Ident) (k : DoElabM Expr) (elabBody : Term → TermElabM Expr) : DoElabM Expr

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

• Lean.Elab.Do.elabWithReassignments letOrReassign vars k = Lean.Elab.Do.declareMutVars? letOrReassign.getLetMutTk? vars do letOrReassign.registerReassignAliasInfo vars k

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

def Lean.Elab.Do.elabDoArrow (letOrReassign : LetOrReassign) (stx : TSyntax [`Lean.Parser.Term.doIdDecl, `Lean.Parser.Term.doPatDecl]) (dec : DoElemCont) : DoElabM Expr

Equations

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

def Lean.Elab.Do.elabDoLet : DoElab

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.