def Lean.Elab.Tactic.evalWithAnnotateState : Tactic

Equations

• Lean.Elab.Tactic.evalWithAnnotateState stx = Lean.Elab.Tactic.withTacticInfoContext stx[1] (Lean.Elab.Term.withNarrowedArgTacticReuse 2 Lean.Elab.Tactic.evalTactic stx)

def Lean.Elab.Tactic.evalDone : Tactic

Equations

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

def Lean.Elab.Tactic.evalSepTactics : Tactic

Evaluates a tactic script in form of a syntax node with alternating tactics and separators as children.

Equations

• Lean.Elab.Tactic.evalSepTactics = Lean.Elab.Tactic.evalSepTactics.goEven

partial def Lean.Elab.Tactic.evalSepTactics.goEven (stx : Syntax) : TacticM Unit

partial def Lean.Elab.Tactic.evalSepTactics.goOdd (stx : Syntax) : TacticM Unit

def Lean.Elab.Tactic.evalSeq1 : Tactic

Equations

• Lean.Elab.Tactic.evalSeq1 stx = Lean.Elab.Tactic.evalSepTactics stx[0]

def Lean.Elab.Tactic.evalParen : Tactic

Equations

• Lean.Elab.Tactic.evalParen = Lean.Elab.Term.withNarrowedArgTacticReuse 1 Lean.Elab.Tactic.evalTactic

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

Equations

• Lean.Elab.Tactic.isCheckpointableTactic arg = pure (arg.getKind == `Lean.Parser.Tactic.save)

def Lean.Elab.Tactic.addCheckpoints (stx : Syntax) : TacticM 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.evalTacticSeq1Indented : Tactic

Equations

• Lean.Elab.Tactic.evalTacticSeq1Indented = Lean.Elab.Term.withNarrowedArgTacticReuse 0 Lean.Elab.Tactic.evalSepTactics

def Lean.Elab.Tactic.evalTacticSeqBracketed : Tactic

Equations

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

def Lean.Elab.Tactic.evalTacticCDot : Tactic

Equations

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

def Lean.Elab.Tactic.evalFocus : Tactic

Equations

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

def Lean.Elab.Tactic.evalRotateLeft : Tactic

Equations

• Lean.Elab.Tactic.evalRotateLeft stx = do let __do_lift ← Lean.Elab.Tactic.getGoals Lean.Elab.Tactic.setGoals (__do_lift.rotateLeft (Lean.Elab.Tactic.getOptRotation✝ stx[1]))

def Lean.Elab.Tactic.evalRotateRight : Tactic

Equations

• Lean.Elab.Tactic.evalRotateRight stx = do let __do_lift ← Lean.Elab.Tactic.getGoals Lean.Elab.Tactic.setGoals (__do_lift.rotateRight (Lean.Elab.Tactic.getOptRotation✝ stx[1]))

def Lean.Elab.Tactic.evalOpen : Tactic

Equations

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

def Lean.Elab.Tactic.elabSetOption : Tactic

Equations

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

def Lean.Elab.Tactic.evalAllGoals : Tactic

Equations

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

def Lean.Elab.Tactic.evalAnyGoals : Tactic

Equations

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

def Lean.Elab.Tactic.evalTacticSeq : Tactic

Equations

• Lean.Elab.Tactic.evalTacticSeq = Lean.Elab.Term.withNarrowedArgTacticReuse 0 Lean.Elab.Tactic.evalTactic

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

def Lean.Elab.Tactic.evalChoice : Tactic

Equations

• Lean.Elab.Tactic.evalChoice stx = Lean.Elab.Tactic.evalChoiceAux stx.getArgs 0

def Lean.Elab.Tactic.evalSkip : Tactic

Equations

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

def Lean.Elab.Tactic.evalUnknown : Tactic

Equations

• Lean.Elab.Tactic.evalUnknown stx = Lean.Elab.addCompletionInfo (Lean.Elab.CompletionInfo.tactic stx)

def Lean.Elab.Tactic.evalFailIfSuccess : Tactic

Equations

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

def Lean.Elab.Tactic.evalTraceState : 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 : Tactic

Equations

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

def Lean.Elab.Tactic.evalAssumption : Tactic

Equations

• Lean.Elab.Tactic.evalAssumption x✝ = Lean.Elab.Tactic.liftMetaTactic fun (mvarId : Lean.MVarId) => Lean.Meta.withAssignableSyntheticOpaque do mvarId.assumption pure []

def Lean.Elab.Tactic.evalContradiction : Tactic

Equations

• Lean.Elab.Tactic.evalContradiction x✝ = Lean.Elab.Tactic.liftMetaTactic fun (mvarId : Lean.MVarId) => do mvarId.contradiction pure []

def Lean.Elab.Tactic.evalRefl : Tactic

Equations

• Lean.Elab.Tactic.evalRefl x✝ = Lean.Elab.Tactic.liftMetaTactic fun (mvarId : Lean.MVarId) => do mvarId.refl pure []

def Lean.Elab.Tactic.evalIntro : Tactic

Equations

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

def Lean.Elab.Tactic.evalIntro.introStep (ref? : Option Syntax) (n : Name) (typeStx? : Option Syntax := none) : TacticM Unit

Equations

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

def Lean.Elab.Tactic.evalIntroMatch : Tactic

Equations

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

def Lean.Elab.Tactic.evalIntros : Tactic

Equations

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

def Lean.Elab.Tactic.evalRevert : Tactic

Equations

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

def Lean.Elab.Tactic.evalClear : Tactic

Equations

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

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

Equations

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

def Lean.Elab.Tactic.evalSubst : Tactic

Equations

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

def Lean.Elab.Tactic.evalSubstVars : Tactic

Equations

• Lean.Elab.Tactic.evalSubstVars x✝ = Lean.Elab.Tactic.liftMetaTactic fun (mvarId : Lean.MVarId) => do let __do_lift ← Lean.Meta.substVars mvarId pure [__do_lift]

def Lean.Elab.Tactic.evalSubstEqs : Tactic

Equations

• Lean.Elab.Tactic.evalSubstEqs x✝ = Lean.Elab.Tactic.liftMetaTactic1 fun (x : Lean.MVarId) => x.substEqs

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

Equations

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

def Lean.Elab.Tactic.evalCase : Tactic

Equations

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

def Lean.Elab.Tactic.evalCase' : Tactic

Equations

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

def Lean.Elab.Tactic.evalRenameInaccessibles : Tactic

Equations

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

def Lean.Elab.Tactic.evalFirst : Tactic

Equations

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

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

def Lean.Elab.Tactic.evalFail : Tactic

Equations

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

def Lean.Elab.Tactic.evalDbgTrace : Tactic

Equations

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

def Lean.Elab.Tactic.evalSleep : Tactic

Equations

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

def Lean.Elab.Tactic.evalLeft : Tactic

Equations

• Lean.Elab.Tactic.evalLeft _stx = Lean.Elab.Tactic.liftMetaTactic fun (g : Lean.MVarId) => Lean.MVarId.nthConstructor `left 0 (some 2) g

def Lean.Elab.Tactic.evalRight : Tactic

Equations

• Lean.Elab.Tactic.evalRight _stx = Lean.Elab.Tactic.liftMetaTactic fun (g : Lean.MVarId) => Lean.MVarId.nthConstructor `right 1 (some 2) g

def Lean.Elab.Tactic.evalReplace : Tactic

Equations

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

def Lean.Elab.Tactic.evalRunTac : Tactic

Equations

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