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

Equations

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

def Lean.Elab.Tactic.evalSepTactics : Lean.Elab.Tactic.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 : Lean.Syntax) : Lean.Elab.Tactic.TacticM Unit

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

def Lean.Elab.Tactic.evalSeq1 : Lean.Elab.Tactic.Tactic

Equations

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

def Lean.Elab.Tactic.evalParen : Lean.Elab.Tactic.Tactic

Equations

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

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

Equations

• Lean.Elab.Tactic.isCheckpointableTactic arg = pure (arg.getKind == `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.evalTacticSeq1Indented : Lean.Elab.Tactic.Tactic

Equations

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

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.evalTacticCDot : 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 = 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 : Lean.Elab.Tactic.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 : 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 = Lean.Elab.Term.withNarrowedArgTacticReuse 0 Lean.Elab.Tactic.evalTactic

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 stx.getArgs 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 __do_lift ← Lean.Elab.Tactic.getGoals Lean.Elab.addCompletionInfo (Lean.Elab.CompletionInfo.tactic stx __do_lift)

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 : Lean.MVarId) => Lean.Meta.withAssignableSyntheticOpaque do mvarId.assumption pure []

def Lean.Elab.Tactic.evalContradiction : Lean.Elab.Tactic.Tactic

Equations

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

def Lean.Elab.Tactic.evalRefl : Lean.Elab.Tactic.Tactic

Equations

• Lean.Elab.Tactic.evalRefl x = Lean.Elab.Tactic.liftMetaTactic fun (mvarId : Lean.MVarId) => do mvarId.refl 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 : Lake.Name) (typeStx? : optParam (Option Lean.Syntax) none) : 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 : Lean.MVarId) => do let __do_lift ← Lean.Meta.substVars mvarId pure [__do_lift]

def Lean.Elab.Tactic.evalSubstEqs : Lean.Elab.Tactic.Tactic

Equations

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

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

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

Equations

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

def Lean.Elab.Tactic.evalRunTac : Lean.Elab.Tactic.Tactic

Equations

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