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 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.Name.mkStr4 "Lean" "Parser" "Tactic" "save")

def Lean.Elab.Tactic.addCheckpoints (stx : Lean.Syntax) : Lean.Elab.Tactic.TacticM Lean.Syntax

Takes a sepByIndent tactic "; ", and inserts checkpoint blocks for save tactics.

Input:

  a
  b
  save
  c
  d
  save
  e

Output:

  checkpoint
    a
    b
    save
  checkpoint
    c
    d
    save
  e

Equations

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

def Lean.Elab.Tactic.evalSepByIndentTactic (stx : Lean.Syntax) : Lean.Elab.Tactic.TacticM Unit

Evaluate `sepByIndent tactic "; "

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.evalSepByIndentTactic 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 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

• Lean.Elab.Tactic.evalRotateRight stx = let n := Lean.Elab.Tactic.getOptRotation stx[1]; do let a ← Lean.Elab.Tactic.getGoals Lean.Elab.Tactic.setGoals (List.rotateRight a n)

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 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.Meta.withPPForTacticGoal (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.MVarId.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.MVarId.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.Name.mkStr2 "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

• Lean.Elab.Tactic.evalDbgTrace stx = match Lean.Syntax.isStrLit? stx[1] with | none => Lean.Elab.throwIllFormedSyntax | some msg => dbgTrace (toString msg) fun x => pure PUnit.unit

def Lean.Elab.Tactic.evalSleep : Lean.Elab.Tactic.Tactic

Equations

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