Documentation

Lean.Elab.Tactic.BuiltinTactic

def Lean.Elab.Tactic.evalWithAnnotateState:

Lean.Elab.Tactic.Tactic

Equations

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

def Lean.Elab.Tactic.evalDone:

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalDone x = Lean.Elab.Tactic.done

def Lean.Elab.Tactic.evalSeq1:

Lean.Elab.Tactic.Tactic

Equations

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

def Lean.Elab.Tactic.evalParen:

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalParen stx = Lean.Elab.Tactic.evalTactic (Lean.Syntax.getOp stx 1)

def Lean.Elab.Tactic.isCheckpointableTactic (arg : Lean.Syntax) :

Lean.Elab.Tactic.TacticM Bool

Equations

Lean.Elab.Tactic.isCheckpointableTactic arg = let kind := Lean.Syntax.getKind arg; pure (kind == `Lean.Parser.Tactic.save)

def Lean.Elab.Tactic.addCheckpoints (args : Array Lean.Syntax) :

Lean.Elab.Tactic.TacticM (Array Lean.Syntax)

Equations

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

def Lean.Elab.Tactic.addCheckpoints.push (acc : Array Lean.Syntax) (result : Array Lean.Syntax) :

Array Lean.Syntax

Equations

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

partial def Lean.Elab.Tactic.addCheckpoints.go (args : Array Lean.Syntax) (i : Nat) (acc : Array Lean.Syntax) (result : Array Lean.Syntax) :

Lean.Elab.Tactic.TacticM (Array Lean.Syntax)

def Lean.Elab.Tactic.evalManyTacticOptSemi (stx : Lean.Syntax) :

Lean.Elab.Tactic.TacticM Unit

Equations

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

def Lean.Elab.Tactic.evalTacticSeq1Indented:

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalTacticSeq1Indented stx = Lean.Elab.Tactic.evalManyTacticOptSemi (Lean.Syntax.getOp stx 0)

def Lean.Elab.Tactic.evalTacticSeqBracketed:

Lean.Elab.Tactic.Tactic

Equations

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

def Lean.Elab.Tactic.evalFocus:

Lean.Elab.Tactic.Tactic

Equations

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

def Lean.Elab.Tactic.evalRotateLeft:

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalRotateLeft stx = let n := Lean.Elab.Tactic.getOptRotation (Lean.Syntax.getOp stx 1); do let a ← Lean.Elab.Tactic.getGoals Lean.Elab.Tactic.setGoals (List.rotateLeft a n)

def Lean.Elab.Tactic.evalRotateRight:

Lean.Elab.Tactic.Tactic

Equations

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

def Lean.Elab.Tactic.evalOpen:

Lean.Elab.Tactic.Tactic

Equations

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

def Lean.Elab.Tactic.elabSetOption:

Lean.Elab.Tactic.Tactic

Equations

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

def Lean.Elab.Tactic.evalAllGoals:

Lean.Elab.Tactic.Tactic

Equations

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

def Lean.Elab.Tactic.evalAnyGoals:

Lean.Elab.Tactic.Tactic

Equations

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

def Lean.Elab.Tactic.evalTacticSeq:

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalTacticSeq stx = Lean.Elab.Tactic.evalTactic (Lean.Syntax.getOp stx 0)

partial def Lean.Elab.Tactic.evalChoiceAux (tactics : Array Lean.Syntax) (i : Nat) :

Lean.Elab.Tactic.TacticM Unit

def Lean.Elab.Tactic.evalChoice:

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalChoice stx = Lean.Elab.Tactic.evalChoiceAux (Lean.Syntax.getArgs stx) 0

def Lean.Elab.Tactic.evalSkip:

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalSkip x = pure ()

def Lean.Elab.Tactic.evalUnknown:

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalUnknown stx = do let a ← Lean.Elab.Tactic.getGoals Lean.Elab.addCompletionInfo (Lean.Elab.CompletionInfo.tactic stx a)

def Lean.Elab.Tactic.evalFailIfSuccess:

Lean.Elab.Tactic.Tactic

Equations

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

def Lean.Elab.Tactic.evalTraceState:

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalTraceState x = do let gs ← Lean.Elab.Tactic.getUnsolvedGoals Lean.addRawTrace (Lean.Elab.goalsToMessageData gs)

def Lean.Elab.Tactic.evalTraceMessage:

Lean.Elab.Tactic.Tactic

Equations

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

def Lean.Elab.Tactic.evalAssumption:

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalAssumption x = Lean.Elab.Tactic.liftMetaTactic fun mvarId => do Lean.Meta.assumption mvarId pure []

def Lean.Elab.Tactic.evalContradiction:

Lean.Elab.Tactic.Tactic

Equations

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

def Lean.Elab.Tactic.evalRefl:

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalRefl x = Lean.Elab.Tactic.liftMetaTactic fun mvarId => do Lean.Meta.refl mvarId pure []

def Lean.Elab.Tactic.evalIntro:

Lean.Elab.Tactic.Tactic

Equations

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

def Lean.Elab.Tactic.evalIntro.introStep (ref : Option Lean.Syntax) (n : Lean.Name) :

Lean.Elab.Tactic.TacticM Unit

Equations

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

def Lean.Elab.Tactic.evalIntroMatch:

Lean.Elab.Tactic.Tactic

Equations

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

def Lean.Elab.Tactic.evalIntros:

Lean.Elab.Tactic.Tactic

Equations

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

def Lean.Elab.Tactic.evalRevert:

Lean.Elab.Tactic.Tactic

Equations

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

def Lean.Elab.Tactic.evalClear:

Lean.Elab.Tactic.Tactic

Equations

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

def Lean.Elab.Tactic.forEachVar (hs : Array Lean.Syntax) (tac : Lean.MVarId → Lean.FVarId → Lean.MetaM Lean.MVarId) :

Lean.Elab.Tactic.TacticM Unit

Equations

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

def Lean.Elab.Tactic.evalSubst:

Lean.Elab.Tactic.Tactic

Equations

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

def Lean.Elab.Tactic.evalSubstVars:

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalSubstVars x = Lean.Elab.Tactic.liftMetaTactic fun mvarId => do let a ← Lean.Meta.substVars mvarId pure [a]

def Lean.Elab.Tactic.renameInaccessibles (mvarId : Lean.MVarId) (hs : Lean.TSyntaxArray `Lean.binderIdent) :

Lean.Elab.Tactic.TacticM Lean.MVarId

Equations

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

def Lean.Elab.Tactic.evalCase:

Lean.Elab.Tactic.Tactic

Equations

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

def Lean.Elab.Tactic.evalCase':

Lean.Elab.Tactic.Tactic

Equations

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

def Lean.Elab.Tactic.evalRenameInaccessibles:

Lean.Elab.Tactic.Tactic

Equations

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

def Lean.Elab.Tactic.evalFirst:

Lean.Elab.Tactic.Tactic

Equations

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

partial def Lean.Elab.Tactic.evalFirst.loop (tacs : Array Lean.Syntax) (i : Nat) :

Lean.Elab.Tactic.TacticM Unit

def Lean.Elab.Tactic.evalFail:

Lean.Elab.Tactic.Tactic

Equations

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

def Lean.Elab.Tactic.evalDbgTrace:

Lean.Elab.Tactic.Tactic

Equations

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

def Lean.Elab.Tactic.evalSleep:

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalSleep stx = match Lean.Syntax.isNatLit? (Lean.Syntax.getOp stx 1) with | none => Lean.Elab.throwIllFormedSyntax | some ms => liftM (IO.sleep (Nat.toUInt32 ms))