Documentation

Lean.Elab.Do

def Lean.Elab.Term.elabLiftMethod:

Lean.Elab.Term.TermElab

Equations

Lean.Elab.Term.elabLiftMethod stx x = Lean.throwErrorAt stx (Lean.toMessageData "invalid use of `(<- ...)`, must be nested inside a 'do' expression")

structure Lean.Elab.Term.ExtractMonadResult:

Type

m : Lean.Expr
α : Lean.Expr
expectedType : Lean.Expr

@[inline]

abbrev Lean.Elab.Term.Do.Var:

Type

Equations

Lean.Elab.Term.Do.Var = Lean.Syntax

structure Lean.Elab.Term.Do.Alt (σ : Type) :

Type

ref : Lean.Syntax
vars : Array Lean.Elab.Term.Do.Var
patterns : Lean.Syntax
rhs : σ

instance Lean.Elab.Term.Do.instInhabitedAlt:

{a : Type} → [inst : Inhabited a] → Inhabited (Lean.Elab.Term.Do.Alt a)

Equations

Lean.Elab.Term.Do.instInhabitedAlt = { default := { ref := default, vars := default, patterns := default, rhs := default } }

inductive Lean.Elab.Term.Do.Code:

Type

decl: Array Lean.Elab.Term.Do.Var → Lean.Syntax → Lean.Elab.Term.Do.Code → Lean.Elab.Term.Do.Code
reassign: Array Lean.Elab.Term.Do.Var → Lean.Syntax → Lean.Elab.Term.Do.Code → Lean.Elab.Term.Do.Code
joinpoint: Lean.Name → Array (Lean.Elab.Term.Do.Var × Bool) → Lean.Elab.Term.Do.Code → Lean.Elab.Term.Do.Code → Lean.Elab.Term.Do.Code
seq: Lean.Syntax → Lean.Elab.Term.Do.Code → Lean.Elab.Term.Do.Code
action: Lean.Syntax → Lean.Elab.Term.Do.Code
break: Lean.Syntax → Lean.Elab.Term.Do.Code
continue: Lean.Syntax → Lean.Elab.Term.Do.Code
return: Lean.Syntax → Lean.Syntax → Lean.Elab.Term.Do.Code
ite: Lean.Syntax → Option Lean.Elab.Term.Do.Var → Lean.Syntax → Lean.Syntax → Lean.Elab.Term.Do.Code → Lean.Elab.Term.Do.Code → Lean.Elab.Term.Do.Code
match: Lean.Syntax → Lean.Syntax → Lean.Syntax → Lean.Syntax → Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Lean.Elab.Term.Do.Code
jmp: Lean.Syntax → Lean.Name → Array Lean.Syntax → Lean.Elab.Term.Do.Code

instance Lean.Elab.Term.Do.instInhabitedCode:

Inhabited Lean.Elab.Term.Do.Code

Equations

Lean.Elab.Term.Do.instInhabitedCode = { default := Lean.Elab.Term.Do.Code.action default }

@[inline]

abbrev Lean.Elab.Term.Do.VarSet:

Type

Equations

Lean.Elab.Term.Do.VarSet = Std.RBMap Lean.Name Lean.Syntax Lean.Name.cmp

structure Lean.Elab.Term.Do.CodeBlock:

Type

code : Lean.Elab.Term.Do.Code
uvars : Lean.Elab.Term.Do.VarSet

def Lean.Elab.Term.Do.CodeBlocl.toMessageData (codeBlock : Lean.Elab.Term.Do.CodeBlock) :

Lean.MessageData

Equations

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

partial def Lean.Elab.Term.Do.CodeBlocl.toMessageData.loop (us : Lean.MessageData) :

Lean.Elab.Term.Do.Code → Lean.MessageData

def Lean.Elab.Term.Do.hasExitPointPred (c : Lean.Elab.Term.Do.Code) (p : Lean.Elab.Term.Do.Code → Bool) :

Equations

Lean.Elab.Term.Do.hasExitPointPred c p = Lean.Elab.Term.Do.hasExitPointPred.loop p c

partial def Lean.Elab.Term.Do.hasExitPointPred.loop (p : Lean.Elab.Term.Do.Code → Bool) :

Lean.Elab.Term.Do.Code → Bool

def Lean.Elab.Term.Do.hasExitPoint (c : Lean.Elab.Term.Do.Code) :

Equations

Lean.Elab.Term.Do.hasExitPoint c = Lean.Elab.Term.Do.hasExitPointPred c fun x => true

def Lean.Elab.Term.Do.hasReturn (c : Lean.Elab.Term.Do.Code) :

Equations

Lean.Elab.Term.Do.hasReturn c = Lean.Elab.Term.Do.hasExitPointPred c fun x => match x with | Lean.Elab.Term.Do.Code.return ref val => true | x => false

def Lean.Elab.Term.Do.hasTerminalAction (c : Lean.Elab.Term.Do.Code) :

Equations

Lean.Elab.Term.Do.hasTerminalAction c = Lean.Elab.Term.Do.hasExitPointPred c fun x => match x with | Lean.Elab.Term.Do.Code.action action => true | x => false

def Lean.Elab.Term.Do.hasBreakContinue (c : Lean.Elab.Term.Do.Code) :

Equations

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

def Lean.Elab.Term.Do.hasBreakContinueReturn (c : Lean.Elab.Term.Do.Code) :

Equations

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

def Lean.Elab.Term.Do.mkAuxDeclFor {m : Type → Type} [inst : Monad m] [inst : Lean.MonadQuotation m] (e : Lean.Syntax) (mkCont : Lean.Syntax → m Lean.Elab.Term.Do.Code) :

m Lean.Elab.Term.Do.Code

Equations

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

def Lean.Elab.Term.Do.convertTerminalActionIntoJmp (code : Lean.Elab.Term.Do.Code) (jp : Lean.Name) (xs : Array Lean.Elab.Term.Do.Var) :

Lean.MacroM Lean.Elab.Term.Do.Code

Equations

Lean.Elab.Term.Do.convertTerminalActionIntoJmp code jp xs = Lean.Elab.Term.Do.convertTerminalActionIntoJmp.loop jp xs code

partial def Lean.Elab.Term.Do.convertTerminalActionIntoJmp.loop (jp : Lean.Name) (xs : Array Lean.Elab.Term.Do.Var) :

Lean.Elab.Term.Do.Code → Lean.MacroM Lean.Elab.Term.Do.Code

structure Lean.Elab.Term.Do.JPDecl:

Type

name : Lean.Name
params : Array (Lean.Elab.Term.Do.Var × Bool)
body : Lean.Elab.Term.Do.Code

def Lean.Elab.Term.Do.attachJP (jpDecl : Lean.Elab.Term.Do.JPDecl) (k : Lean.Elab.Term.Do.Code) :

Lean.Elab.Term.Do.Code

Equations

Lean.Elab.Term.Do.attachJP jpDecl k = Lean.Elab.Term.Do.Code.joinpoint jpDecl.name jpDecl.params jpDecl.body k

def Lean.Elab.Term.Do.attachJPs (jpDecls : Array Lean.Elab.Term.Do.JPDecl) (k : Lean.Elab.Term.Do.Code) :

Lean.Elab.Term.Do.Code

Equations

Lean.Elab.Term.Do.attachJPs jpDecls k = Array.foldr Lean.Elab.Term.Do.attachJP k jpDecls (Array.size jpDecls)

def Lean.Elab.Term.Do.mkFreshJP (ps : Array (Lean.Elab.Term.Do.Var × Bool)) (body : Lean.Elab.Term.Do.Code) :

Lean.Elab.TermElabM Lean.Elab.Term.Do.JPDecl

Equations

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

def Lean.Elab.Term.Do.addFreshJP (ps : Array (Lean.Elab.Term.Do.Var × Bool)) (body : Lean.Elab.Term.Do.Code) :

StateRefT' IO.RealWorld (Array Lean.Elab.Term.Do.JPDecl) Lean.Elab.TermElabM Lean.Name

Equations

Lean.Elab.Term.Do.addFreshJP ps body = do let jp ← liftM (Lean.Elab.Term.Do.mkFreshJP ps body) modify fun jps => Array.push jps jp pure jp.name

def Lean.Elab.Term.Do.insertVars (rs : Lean.Elab.Term.Do.VarSet) (xs : Array Lean.Elab.Term.Do.Var) :

Lean.Elab.Term.Do.VarSet

Equations

Lean.Elab.Term.Do.insertVars rs xs = Array.foldl (fun rs x => Std.RBMap.insert rs (Lean.Syntax.getId x) x) rs xs 0 (Array.size xs)

def Lean.Elab.Term.Do.eraseVars (rs : Lean.Elab.Term.Do.VarSet) (xs : Array Lean.Elab.Term.Do.Var) :

Lean.Elab.Term.Do.VarSet

Equations

Lean.Elab.Term.Do.eraseVars rs xs = Array.foldl (fun a a_1 => Std.RBMap.erase a (Lean.Syntax.getId a_1)) rs xs 0 (Array.size xs)

def Lean.Elab.Term.Do.eraseOptVar (rs : Lean.Elab.Term.Do.VarSet) (x? : Option Lean.Elab.Term.Do.Var) :

Lean.Elab.Term.Do.VarSet

Equations

Lean.Elab.Term.Do.eraseOptVar rs x? = match x? with | none => rs | some x => Std.RBMap.insert rs (Lean.Syntax.getId x) x

def Lean.Elab.Term.Do.mkSimpleJmp (ref : Lean.Syntax) (rs : Lean.Elab.Term.Do.VarSet) (c : Lean.Elab.Term.Do.Code) :

StateRefT' IO.RealWorld (Array Lean.Elab.Term.Do.JPDecl) Lean.Elab.TermElabM Lean.Elab.Term.Do.Code

Equations

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

def Lean.Elab.Term.Do.mkJmp (ref : Lean.Syntax) (rs : Lean.Elab.Term.Do.VarSet) (val : Lean.Syntax) (mkJPBody : Lean.Syntax → Lean.MacroM Lean.Elab.Term.Do.Code) :

StateRefT' IO.RealWorld (Array Lean.Elab.Term.Do.JPDecl) Lean.Elab.TermElabM Lean.Elab.Term.Do.Code

Equations

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

partial def Lean.Elab.Term.Do.pullExitPointsAux:

Lean.Elab.Term.Do.VarSet → Lean.Elab.Term.Do.Code → StateRefT' IO.RealWorld (Array Lean.Elab.Term.Do.JPDecl) Lean.Elab.TermElabM Lean.Elab.Term.Do.Code

def Lean.Elab.Term.Do.pullExitPoints (c : Lean.Elab.Term.Do.Code) :

Lean.Elab.TermElabM Lean.Elab.Term.Do.Code

Equations

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

def Lean.Elab.Term.Do.extendUpdatedVarsAux (c : Lean.Elab.Term.Do.Code) (ws : Lean.Elab.Term.Do.VarSet) :

Lean.Elab.TermElabM Lean.Elab.Term.Do.Code

Equations

Lean.Elab.Term.Do.extendUpdatedVarsAux c ws = Lean.Elab.Term.Do.extendUpdatedVarsAux.update ws c

partial def Lean.Elab.Term.Do.extendUpdatedVarsAux.update (ws : Lean.Elab.Term.Do.VarSet) :

Lean.Elab.Term.Do.Code → Lean.Elab.TermElabM Lean.Elab.Term.Do.Code

def Lean.Elab.Term.Do.extendUpdatedVars (c : Lean.Elab.Term.Do.CodeBlock) (ws : Lean.Elab.Term.Do.VarSet) :

Lean.Elab.TermElabM Lean.Elab.Term.Do.CodeBlock

Equations

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

def Lean.Elab.Term.Do.homogenize (c₁ : Lean.Elab.Term.Do.CodeBlock) (c₂ : Lean.Elab.Term.Do.CodeBlock) :

Lean.Elab.TermElabM (Lean.Elab.Term.Do.CodeBlock × Lean.Elab.Term.Do.CodeBlock)

Equations

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

def Lean.Elab.Term.Do.mkVarDeclCore (xs : Array Lean.Elab.Term.Do.Var) (stx : Lean.Syntax) (c : Lean.Elab.Term.Do.CodeBlock) :

Lean.Elab.Term.Do.CodeBlock

Equations

Lean.Elab.Term.Do.mkVarDeclCore xs stx c = { code := Lean.Elab.Term.Do.Code.decl xs stx c.code, uvars := Lean.Elab.Term.Do.eraseVars c.uvars xs }

def Lean.Elab.Term.Do.mkReassignCore (xs : Array Lean.Elab.Term.Do.Var) (stx : Lean.Syntax) (c : Lean.Elab.Term.Do.CodeBlock) :

Lean.Elab.TermElabM Lean.Elab.Term.Do.CodeBlock

Equations

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

def Lean.Elab.Term.Do.mkSeq (action : Lean.Syntax) (c : Lean.Elab.Term.Do.CodeBlock) :

Lean.Elab.Term.Do.CodeBlock

Equations

Lean.Elab.Term.Do.mkSeq action c = { code := Lean.Elab.Term.Do.Code.seq action c.code, uvars := c.uvars }

def Lean.Elab.Term.Do.mkTerminalAction (action : Lean.Syntax) :

Lean.Elab.Term.Do.CodeBlock

Equations

Lean.Elab.Term.Do.mkTerminalAction action = { code := Lean.Elab.Term.Do.Code.action action, uvars := ∅ }

def Lean.Elab.Term.Do.mkReturn (ref : Lean.Syntax) (val : Lean.Syntax) :

Lean.Elab.Term.Do.CodeBlock

Equations

Lean.Elab.Term.Do.mkReturn ref val = { code := Lean.Elab.Term.Do.Code.return ref val, uvars := ∅ }

def Lean.Elab.Term.Do.mkBreak (ref : Lean.Syntax) :

Lean.Elab.Term.Do.CodeBlock

Equations

Lean.Elab.Term.Do.mkBreak ref = { code := Lean.Elab.Term.Do.Code.break ref, uvars := ∅ }

def Lean.Elab.Term.Do.mkContinue (ref : Lean.Syntax) :

Lean.Elab.Term.Do.CodeBlock

Equations

Lean.Elab.Term.Do.mkContinue ref = { code := Lean.Elab.Term.Do.Code.continue ref, uvars := ∅ }

def Lean.Elab.Term.Do.mkIte (ref : Lean.Syntax) (optIdent : Lean.Syntax) (cond : Lean.Syntax) (thenBranch : Lean.Elab.Term.Do.CodeBlock) (elseBranch : Lean.Elab.Term.Do.CodeBlock) :

Lean.Elab.TermElabM Lean.Elab.Term.Do.CodeBlock

Equations

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

def Lean.Elab.Term.Do.mkPureUnitAction:

Lean.MacroM Lean.Elab.Term.Do.CodeBlock

Equations

Lean.Elab.Term.Do.mkPureUnitAction = do let a ← Lean.Elab.Term.Do.mkPureUnit pure (Lean.Elab.Term.Do.mkTerminalAction a)

def Lean.Elab.Term.Do.mkUnless (cond : Lean.Syntax) (c : Lean.Elab.Term.Do.CodeBlock) :

Lean.MacroM Lean.Elab.Term.Do.CodeBlock

Equations

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

def Lean.Elab.Term.Do.mkMatch (ref : Lean.Syntax) (genParam : Lean.Syntax) (discrs : Lean.Syntax) (optMotive : Lean.Syntax) (alts : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.CodeBlock)) :

Lean.Elab.TermElabM Lean.Elab.Term.Do.CodeBlock

Equations

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

def Lean.Elab.Term.Do.concat (terminal : Lean.Elab.Term.Do.CodeBlock) (kRef : Lean.Syntax) (y? : Option Lean.Elab.Term.Do.Var) (k : Lean.Elab.Term.Do.CodeBlock) :

Lean.Elab.TermElabM Lean.Elab.Term.Do.CodeBlock

Equations

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

def Lean.Elab.Term.Do.getLetIdDeclVar (letIdDecl : Lean.Syntax) :

Lean.Elab.Term.Do.Var

Equations

Lean.Elab.Term.Do.getLetIdDeclVar letIdDecl = Lean.Syntax.getOp letIdDecl 0

def Lean.Elab.Term.Do.getPatternVarsEx (pattern : Lean.Syntax) :

Lean.Elab.TermElabM (Array Lean.Elab.Term.Do.Var)

Equations

Lean.Elab.Term.Do.getPatternVarsEx pattern = HOrElse.hOrElse (Lean.Elab.Term.getPatternVars pattern) fun x => Lean.Elab.Term.Quotation.getPatternVars pattern

def Lean.Elab.Term.Do.getPatternsVarsEx (patterns : Array Lean.Syntax) :

Lean.Elab.TermElabM (Array Lean.Elab.Term.Do.Var)

Equations

Lean.Elab.Term.Do.getPatternsVarsEx patterns = HOrElse.hOrElse (Lean.Elab.Term.getPatternsVars patterns) fun x => Lean.Elab.Term.Quotation.getPatternsVars patterns

def Lean.Elab.Term.Do.getLetPatDeclVars (letPatDecl : Lean.Syntax) :

Lean.Elab.TermElabM (Array Lean.Elab.Term.Do.Var)

Equations

Lean.Elab.Term.Do.getLetPatDeclVars letPatDecl = let pattern := Lean.Syntax.getOp letPatDecl 0; Lean.Elab.Term.Do.getPatternVarsEx pattern

def Lean.Elab.Term.Do.getLetEqnsDeclVar (letEqnsDecl : Lean.Syntax) :

Lean.Elab.Term.Do.Var

Equations

Lean.Elab.Term.Do.getLetEqnsDeclVar letEqnsDecl = Lean.Syntax.getOp letEqnsDecl 0

def Lean.Elab.Term.Do.getLetDeclVars (letDecl : Lean.Syntax) :

Lean.Elab.TermElabM (Array Lean.Elab.Term.Do.Var)

Equations

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

def Lean.Elab.Term.Do.getDoLetVars (doLet : Lean.Syntax) :

Lean.Elab.TermElabM (Array Lean.Elab.Term.Do.Var)

Equations

Lean.Elab.Term.Do.getDoLetVars doLet = Lean.Elab.Term.Do.getLetDeclVars (Lean.Syntax.getOp doLet 2)

def Lean.Elab.Term.Do.getHaveIdLhsVar (optIdent : Lean.Syntax) :

Lean.Elab.TermElabM Lean.Elab.Term.Do.Var

Equations

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

def Lean.Elab.Term.Do.getDoHaveVars (doHave : Lean.Syntax) :

Lean.Elab.TermElabM (Array Lean.Elab.Term.Do.Var)

Equations

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

def Lean.Elab.Term.Do.getDoLetRecVars (doLetRec : Lean.Syntax) :

Lean.Elab.TermElabM (Array Lean.Elab.Term.Do.Var)

Equations

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

def Lean.Elab.Term.Do.getDoIdDeclVar (doIdDecl : Lean.Syntax) :

Lean.Elab.Term.Do.Var

Equations

Lean.Elab.Term.Do.getDoIdDeclVar doIdDecl = Lean.Syntax.getOp doIdDecl 0

def Lean.Elab.Term.Do.getDoPatDeclVars (doPatDecl : Lean.Syntax) :

Lean.Elab.TermElabM (Array Lean.Elab.Term.Do.Var)

Equations

Lean.Elab.Term.Do.getDoPatDeclVars doPatDecl = let pattern := Lean.Syntax.getOp doPatDecl 0; Lean.Elab.Term.Do.getPatternVarsEx pattern

def Lean.Elab.Term.Do.getDoLetArrowVars (doLetArrow : Lean.Syntax) :

Lean.Elab.TermElabM (Array Lean.Elab.Term.Do.Var)

Equations

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

def Lean.Elab.Term.Do.getDoReassignVars (doReassign : Lean.Syntax) :

Lean.Elab.TermElabM (Array Lean.Elab.Term.Do.Var)

Equations

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

def Lean.Elab.Term.Do.mkDoSeq (doElems : Array Lean.Syntax) :

Equations

Lean.Elab.Term.Do.mkDoSeq doElems = (Lean.mkNode `Lean.Parser.Term.doSeqIndent #[Lean.mkNullNode (Array.map (fun doElem => Lean.mkNullNode #[doElem, Lean.mkNullNode]) doElems)]).raw

def Lean.Elab.Term.Do.mkSingletonDoSeq (doElem : Lean.Syntax) :

Equations

Lean.Elab.Term.Do.mkSingletonDoSeq doElem = Lean.Elab.Term.Do.mkDoSeq #[doElem]

structure Lean.Elab.Term.Do.DoIfView:

Type

ref : Lean.Syntax
optIdent : Lean.Syntax
cond : Lean.Syntax
thenBranch : Lean.Syntax
elseBranch : Lean.Syntax

def Lean.Elab.Term.Do.isDoExpr? (doElem : Lean.Syntax) :

Option Lean.Syntax

Equations

Lean.Elab.Term.Do.isDoExpr? doElem = if (Lean.Syntax.getKind doElem == `Lean.Parser.Term.doExpr) = true then some (Lean.Syntax.getOp doElem 0) else none

inductive Lean.Elab.Term.Do.ToTerm.Kind:

Type

regular: Lean.Elab.Term.Do.ToTerm.Kind
forIn: Lean.Elab.Term.Do.ToTerm.Kind
forInWithReturn: Lean.Elab.Term.Do.ToTerm.Kind
nestedBC: Lean.Elab.Term.Do.ToTerm.Kind
nestedPR: Lean.Elab.Term.Do.ToTerm.Kind
nestedSBC: Lean.Elab.Term.Do.ToTerm.Kind
nestedPRBC: Lean.Elab.Term.Do.ToTerm.Kind

instance Lean.Elab.Term.Do.ToTerm.instInhabitedKind:

Inhabited Lean.Elab.Term.Do.ToTerm.Kind

Equations

Lean.Elab.Term.Do.ToTerm.instInhabitedKind = { default := Lean.Elab.Term.Do.ToTerm.Kind.regular }

def Lean.Elab.Term.Do.ToTerm.Kind.isRegular:

Lean.Elab.Term.Do.ToTerm.Kind → Bool

Equations

Lean.Elab.Term.Do.ToTerm.Kind.isRegular _fun_discr = match _fun_discr with | Lean.Elab.Term.Do.ToTerm.Kind.regular => true | x => false

structure Lean.Elab.Term.Do.ToTerm.Context:

Type

@[inline]

abbrev Lean.Elab.Term.Do.ToTerm.M (α : Type) :

Type

Equations

Lean.Elab.Term.Do.ToTerm.M = ReaderT Lean.Elab.Term.Do.ToTerm.Context Lean.MacroM

def Lean.Elab.Term.Do.ToTerm.mkUVarTuple:

Lean.Elab.Term.Do.ToTerm.M Lean.Syntax

Equations

Lean.Elab.Term.Do.ToTerm.mkUVarTuple = do let ctx ← read liftM (Lean.Elab.Term.Do.mkTuple ctx.uvars)

def Lean.Elab.Term.Do.ToTerm.returnToTerm (val : Lean.Syntax) :

Lean.Elab.Term.Do.ToTerm.M Lean.Syntax

Equations

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

def Lean.Elab.Term.Do.ToTerm.continueToTerm:

Lean.Elab.Term.Do.ToTerm.M Lean.Syntax

Equations

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

def Lean.Elab.Term.Do.ToTerm.breakToTerm:

Lean.Elab.Term.Do.ToTerm.M Lean.Syntax

Equations

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

def Lean.Elab.Term.Do.ToTerm.actionTerminalToTerm (action : Lean.Syntax) :

Lean.Elab.Term.Do.ToTerm.M Lean.Syntax

Equations

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

def Lean.Elab.Term.Do.ToTerm.seqToTerm (action : Lean.Syntax) (k : Lean.Syntax) :

Lean.Elab.Term.Do.ToTerm.M Lean.Syntax

Equations

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

def Lean.Elab.Term.Do.ToTerm.declToTerm (decl : Lean.Syntax) (k : Lean.Syntax) :

Lean.Elab.Term.Do.ToTerm.M Lean.Syntax

Equations

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

def Lean.Elab.Term.Do.ToTerm.reassignToTerm (reassign : Lean.Syntax) (k : Lean.Syntax) :

Lean.MacroM Lean.Syntax

Equations

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

def Lean.Elab.Term.Do.ToTerm.mkIte (optIdent : Lean.Syntax) (cond : Lean.Syntax) (thenBranch : Lean.Syntax) (elseBranch : Lean.Syntax) :

Lean.MacroM Lean.Syntax

Equations

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

def Lean.Elab.Term.Do.ToTerm.mkJoinPoint (j : Lean.Name) (ps : Array (Lean.Syntax × Bool)) (body : Lean.Syntax) (k : Lean.Syntax) :

Lean.Elab.Term.Do.ToTerm.M Lean.Syntax

Equations

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

def Lean.Elab.Term.Do.ToTerm.mkJmp (ref : Lean.Syntax) (j : Lean.Name) (args : Array Lean.Syntax) :

Equations

Lean.Elab.Term.Do.ToTerm.mkJmp ref j args = (Lean.Syntax.mkApp { raw := (Lean.mkIdentFrom ref j).raw } (Lean.TSyntaxArray.mk args)).raw

partial def Lean.Elab.Term.Do.ToTerm.toTerm (c : Lean.Elab.Term.Do.Code) :

Lean.Elab.Term.Do.ToTerm.M Lean.Syntax

def Lean.Elab.Term.Do.ToTerm.run (code : Lean.Elab.Term.Do.Code) (m : Lean.Syntax) (uvars : optParam (Array Lean.Elab.Term.Do.Var) #[]) (kind : optParam Lean.Elab.Term.Do.ToTerm.Kind Lean.Elab.Term.Do.ToTerm.Kind.regular) :

Lean.MacroM Lean.Syntax

Equations

Lean.Elab.Term.Do.ToTerm.run code m uvars kind = Lean.Elab.Term.Do.ToTerm.toTerm code { m := m, uvars := uvars, kind := kind }

def Lean.Elab.Term.Do.ToTerm.mkNestedKind (a : Bool) (r : Bool) (bc : Bool) :

Lean.Elab.Term.Do.ToTerm.Kind

Equations

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

def Lean.Elab.Term.Do.ToTerm.mkNestedTerm (code : Lean.Elab.Term.Do.Code) (m : Lean.Syntax) (uvars : Array Lean.Elab.Term.Do.Var) (a : Bool) (r : Bool) (bc : Bool) :

Lean.MacroM Lean.Syntax

Equations

Lean.Elab.Term.Do.ToTerm.mkNestedTerm code m uvars a r bc = Lean.Elab.Term.Do.ToTerm.run code m uvars (Lean.Elab.Term.Do.ToTerm.mkNestedKind a r bc)

def Lean.Elab.Term.Do.ToTerm.matchNestedTermResult (term : Lean.Syntax) (uvars : Array Lean.Elab.Term.Do.Var) (a : Bool) (r : Bool) (bc : Bool) :

Lean.MacroM (List Lean.Syntax)

Equations

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

def Lean.Elab.Term.Do.isMutableLet (doElem : Lean.Syntax) :

Equations

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

structure Lean.Elab.Term.Do.ToCodeBlock.Context:

Type

ref : Lean.Syntax
m : Lean.Syntax
mutableVars : Lean.Elab.Term.Do.VarSet
insideFor : Bool

@[inline]

abbrev Lean.Elab.Term.Do.ToCodeBlock.M (α : Type) :

Type

Equations

Lean.Elab.Term.Do.ToCodeBlock.M = ReaderT Lean.Elab.Term.Do.ToCodeBlock.Context Lean.Elab.TermElabM

def Lean.Elab.Term.Do.ToCodeBlock.withNewMutableVars {α : Type} (newVars : Array Lean.Elab.Term.Do.Var) (mutable : Bool) (x : Lean.Elab.Term.Do.ToCodeBlock.M α) :

Lean.Elab.Term.Do.ToCodeBlock.M α

Equations

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

def Lean.Elab.Term.Do.ToCodeBlock.checkReassignable (xs : Array Lean.Elab.Term.Do.Var) :

Lean.Elab.Term.Do.ToCodeBlock.M Unit

Equations

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

def Lean.Elab.Term.Do.ToCodeBlock.checkNotShadowingMutable (xs : Array Lean.Elab.Term.Do.Var) :

Lean.Elab.Term.Do.ToCodeBlock.M Unit

Equations

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

def Lean.Elab.Term.Do.ToCodeBlock.withFor {α : Type} (x : Lean.Elab.Term.Do.ToCodeBlock.M α) :

Lean.Elab.Term.Do.ToCodeBlock.M α

Equations

Lean.Elab.Term.Do.ToCodeBlock.withFor x = withReader (fun ctx => { ref := ctx.ref, m := ctx.m, mutableVars := ctx.mutableVars, insideFor := true }) x

structure Lean.Elab.Term.Do.ToCodeBlock.ToForInTermResult:

Type

uvars : Array Lean.Elab.Term.Do.Var
term : Lean.Syntax

def Lean.Elab.Term.Do.ToCodeBlock.mkForInBody:

Lean.Syntax → Lean.Elab.Term.Do.CodeBlock → Lean.Elab.Term.Do.ToCodeBlock.M Lean.Elab.Term.Do.ToCodeBlock.ToForInTermResult

Equations

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

def Lean.Elab.Term.Do.ToCodeBlock.ensureInsideFor:

Lean.Elab.Term.Do.ToCodeBlock.M Unit

Equations

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

def Lean.Elab.Term.Do.ToCodeBlock.ensureEOS (doElems : List Lean.Syntax) :

Lean.Elab.Term.Do.ToCodeBlock.M Unit

Equations

Lean.Elab.Term.Do.ToCodeBlock.ensureEOS doElems = if List.isEmpty doElems = true then pure PUnit.unit else Lean.throwError (Lean.toMessageData "must be last element in a 'do' sequence")

def Lean.Elab.Term.Do.ToCodeBlock.expandLiftMethod (doElem : Lean.Syntax) :

Lean.Elab.Term.Do.ToCodeBlock.M (List Lean.Syntax × Lean.Syntax)

Equations

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

def Lean.Elab.Term.Do.ToCodeBlock.checkLetArrowRHS (doElem : Lean.Syntax) :

Lean.Elab.Term.Do.ToCodeBlock.M Unit

Equations

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

def Lean.Elab.Term.Do.ToCodeBlock.doReturnToCode (doReturn : Lean.Syntax) (doElems : List Lean.Syntax) :

Lean.Elab.Term.Do.ToCodeBlock.M Lean.Elab.Term.Do.CodeBlock

Equations

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

structure Lean.Elab.Term.Do.ToCodeBlock.Catch:

Type

def Lean.Elab.Term.Do.ToCodeBlock.getTryCatchUpdatedVars (tryCode : Lean.Elab.Term.Do.CodeBlock) (catches : Array Lean.Elab.Term.Do.ToCodeBlock.Catch) (finallyCode? : Option Lean.Elab.Term.Do.CodeBlock) :

Lean.Elab.Term.Do.VarSet

Equations

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

def Lean.Elab.Term.Do.ToCodeBlock.tryCatchPred (tryCode : Lean.Elab.Term.Do.CodeBlock) (catches : Array Lean.Elab.Term.Do.ToCodeBlock.Catch) (finallyCode? : Option Lean.Elab.Term.Do.CodeBlock) (p : Lean.Elab.Term.Do.Code → Bool) :

Equations

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

partial def Lean.Elab.Term.Do.ToCodeBlock.concatWith (c : Lean.Elab.Term.Do.CodeBlock) (doElems : List Lean.Syntax) :

Lean.Elab.Term.Do.ToCodeBlock.M Lean.Elab.Term.Do.CodeBlock

partial def Lean.Elab.Term.Do.ToCodeBlock.doLetArrowToCode (doLetArrow : Lean.Syntax) (doElems : List Lean.Syntax) :

Lean.Elab.Term.Do.ToCodeBlock.M Lean.Elab.Term.Do.CodeBlock

partial def Lean.Elab.Term.Do.ToCodeBlock.doLetElseToCode (doLetElse : Lean.Syntax) (doElems : List Lean.Syntax) :

Lean.Elab.Term.Do.ToCodeBlock.M Lean.Elab.Term.Do.CodeBlock

partial def Lean.Elab.Term.Do.ToCodeBlock.doReassignArrowToCode (doReassignArrow : Lean.Syntax) (doElems : List Lean.Syntax) :

Lean.Elab.Term.Do.ToCodeBlock.M Lean.Elab.Term.Do.CodeBlock

partial def Lean.Elab.Term.Do.ToCodeBlock.doIfToCode (doIf : Lean.Syntax) (doElems : List Lean.Syntax) :

Lean.Elab.Term.Do.ToCodeBlock.M Lean.Elab.Term.Do.CodeBlock

partial def Lean.Elab.Term.Do.ToCodeBlock.doUnlessToCode (doUnless : Lean.Syntax) (doElems : List Lean.Syntax) :

Lean.Elab.Term.Do.ToCodeBlock.M Lean.Elab.Term.Do.CodeBlock

partial def Lean.Elab.Term.Do.ToCodeBlock.doForToCode (doFor : Lean.Syntax) (doElems : List Lean.Syntax) :

Lean.Elab.Term.Do.ToCodeBlock.M Lean.Elab.Term.Do.CodeBlock

partial def Lean.Elab.Term.Do.ToCodeBlock.doMatchToCode (doMatch : Lean.Syntax) (doElems : List Lean.Syntax) :

Lean.Elab.Term.Do.ToCodeBlock.M Lean.Elab.Term.Do.CodeBlock

Generate CodeBlock for doMatch; doElems

partial def Lean.Elab.Term.Do.ToCodeBlock.doTryToCode (doTry : Lean.Syntax) (doElems : List Lean.Syntax) :

Lean.Elab.Term.Do.ToCodeBlock.M Lean.Elab.Term.Do.CodeBlock

Generate CodeBlock for doTry; doElems def doTry := leading_parser "try " >> doSeq >> many (doCatch <|> doCatchMatch) >> optional doFinally def doCatch := leading_parser "catch " >> binderIdent >> optional (":" >> termParser) >> darrow >> doSeq def doCatchMatch := leading_parser "catch " >> doMatchAlts def doFinally := leading_parser "finally " >> doSeq

partial def Lean.Elab.Term.Do.ToCodeBlock.doSeqToCode:

List Lean.Syntax → Lean.Elab.Term.Do.ToCodeBlock.M Lean.Elab.Term.Do.CodeBlock

def Lean.Elab.Term.Do.ToCodeBlock.run (doStx : Lean.Syntax) (m : Lean.Syntax) :

Lean.Elab.TermElabM Lean.Elab.Term.Do.CodeBlock

Equations

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

def Lean.Elab.Term.Do.elabDo:

Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.expandTermFor:

Equations

Lean.Elab.Term.expandTermFor = Lean.Elab.Term.toDoElem `Lean.Parser.Term.doFor

def Lean.Elab.Term.expandTermTry:

Equations

Lean.Elab.Term.expandTermTry = Lean.Elab.Term.toDoElem `Lean.Parser.Term.doTry

def Lean.Elab.Term.expandTermUnless:

Equations

Lean.Elab.Term.expandTermUnless = Lean.Elab.Term.toDoElem `Lean.Parser.Term.doUnless

def Lean.Elab.Term.expandTermReturn:

Equations

Lean.Elab.Term.expandTermReturn = Lean.Elab.Term.toDoElem `Lean.Parser.Term.doReturn