def Aesop.Script.Tactic.skip : Aesop.Script.Tactic

Equations

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

def Aesop.Script.TacticBuilder.applyStx (e : Lean.Term) (md : Lean.Meta.TransparencyMode) : Aesop.Script.TacticBuilder

Equations

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

def Aesop.Script.TacticBuilder.apply (mvarId : Lean.MVarId) (e : Lean.Expr) (md : Lean.Meta.TransparencyMode) : Aesop.Script.TacticBuilder

Equations

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

def Aesop.Script.TacticBuilder.exactFVar (goal : Lean.MVarId) (fvarId : Lean.FVarId) (md : Lean.Meta.TransparencyMode) : Aesop.Script.TacticBuilder

Equations

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

def Aesop.Script.TacticBuilder.replace (preGoal : Lean.MVarId) (postGoal : Lean.MVarId) (fvarId : Lean.FVarId) (type : Lean.Expr) (proof : Lean.Expr) : Aesop.Script.TacticBuilder

Equations

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

def Aesop.Script.TacticBuilder.assertHypothesis (goal : Lean.MVarId) (h : Lean.Meta.Hypothesis) (md : Lean.Meta.TransparencyMode) : Aesop.Script.TacticBuilder

Equations

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

def Aesop.Script.TacticBuilder.clear (goal : Lean.MVarId) (fvarIds : Array Lean.FVarId) : Aesop.Script.TacticBuilder

Equations

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

def Aesop.Script.TacticBuilder.cases (goal : Lean.MVarId) (e : Lean.Expr) (ctorNames : Array Aesop.CtorNames) : Aesop.Script.TacticBuilder

Equations

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

def Aesop.Script.TacticBuilder.obtain (goal : Lean.MVarId) (e : Lean.Expr) (ctorNames : Aesop.CtorNames) : Aesop.Script.TacticBuilder

Equations

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

def Aesop.Script.TacticBuilder.casesOrObtain (goal : Lean.MVarId) (e : Lean.Expr) (ctorNames : Array Aesop.CtorNames) : Aesop.Script.TacticBuilder

Equations

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

def Aesop.Script.TacticBuilder.renameInaccessibleFVars (postGoal : Lean.MVarId) (renamedFVars : Array Lean.FVarId) : Aesop.Script.TacticBuilder

Equations

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

def Aesop.Script.TacticBuilder.aesopUnfold (usedDecls : Lean.HashSet Lean.Name) : Aesop.Script.TacticBuilder

Equations

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

def Aesop.Script.TacticBuilder.extN (r : Aesop.ExtResult) : Aesop.Script.TacticBuilder

Equations

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

def Aesop.Script.TacticBuilder.extN.mkPat (fvarId : Lean.FVarId) : Lean.MetaM (Lean.TSyntax `rintroPat)

Equations

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

def Aesop.Script.TacticBuilder.simpAllOrSimpAtStarOnly (simpAll : Bool) (inGoal : Lean.MVarId) (configStx? : Option Lean.Term) (usedTheorems : Lean.Meta.Simp.UsedSimps) : Aesop.Script.TacticBuilder

Equations

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

def Aesop.Script.TacticBuilder.intros (postGoal : Lean.MVarId) (newFVarIds : Array Lean.FVarId) (md : Lean.Meta.TransparencyMode) : Aesop.Script.TacticBuilder

Equations

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

def Aesop.Script.TacticBuilder.splitTarget : Aesop.Script.TacticBuilder

Equations

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

def Aesop.Script.TacticBuilder.splitAt (goal : Lean.MVarId) (fvarId : Lean.FVarId) : Aesop.Script.TacticBuilder

Equations

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

def Aesop.Script.TacticBuilder.substFVars (goal : Lean.MVarId) (fvarIds : Array Lean.FVarId) : Aesop.Script.TacticBuilder

Equations

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

def Aesop.assertHypothesisS (goal : Lean.MVarId) (h : Lean.Meta.Hypothesis) (md : Lean.Meta.TransparencyMode) : Aesop.ScriptM (Lean.MVarId × Array Lean.FVarId)

Equations

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

def Aesop.assertHypothesisS.tacticBuilder (goal : Lean.MVarId) (h : Lean.Meta.Hypothesis) (md : Lean.Meta.TransparencyMode) : Lean.MVarId × Array Lean.FVarId → Aesop.Script.TacticBuilder

Equations

• Aesop.assertHypothesisS.tacticBuilder goal h md x = Aesop.Script.TacticBuilder.assertHypothesis goal h md

def Aesop.applyS (goal : Lean.MVarId) (e : Lean.Expr) (eStx? : Option Lean.Term) (md : Lean.Meta.TransparencyMode) : Aesop.ScriptM (Array Lean.MVarId)

Equations

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

def Aesop.applyS.tacticBuilder (goal : Lean.MVarId) (e : Lean.Expr) (eStx? : Option Lean.Term) (md : Lean.Meta.TransparencyMode) : Array Lean.MVarId → Aesop.Script.TacticBuilder

Equations

• Aesop.applyS.tacticBuilder goal e eStx? md x = match eStx? with | none => Aesop.Script.TacticBuilder.apply goal e md | some eStx => Aesop.Script.TacticBuilder.applyStx eStx md

def Aesop.replaceFVarS (goal : Lean.MVarId) (fvarId : Lean.FVarId) (type : Lean.Expr) (proof : Lean.Expr) : Aesop.ScriptM (Lean.MVarId × Lean.FVarId)

Equations

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

def Aesop.replaceFVarS.tacticBuilder (goal : Lean.MVarId) (fvarId : Lean.FVarId) (type : Lean.Expr) (proof : Lean.Expr) : Lean.MVarId × Lean.FVarId → Aesop.Script.TacticBuilder

Equations

• Aesop.replaceFVarS.tacticBuilder goal fvarId type proof x = Aesop.Script.TacticBuilder.replace goal x.fst fvarId type proof

def Aesop.clearS (goal : Lean.MVarId) (fvarId : Lean.FVarId) : Aesop.ScriptM Lean.MVarId

Equations

• Aesop.clearS goal fvarId = Aesop.withScriptStep goal (fun (x : Lean.MVarId) => #[x]) (fun (x : Lean.MVarId) => true) (Aesop.clearS.tacticBuilder goal fvarId) (goal.clear fvarId)

def Aesop.clearS.tacticBuilder (goal : Lean.MVarId) (fvarId : Lean.FVarId) : Lean.MVarId → Aesop.Script.TacticBuilder

Equations

• Aesop.clearS.tacticBuilder goal fvarId x = Aesop.Script.TacticBuilder.clear goal #[fvarId]

def Aesop.tryClearS (goal : Lean.MVarId) (fvarId : Lean.FVarId) : Aesop.ScriptM (Option Lean.MVarId)

Equations

• Aesop.tryClearS goal fvarId = Aesop.withOptScriptStep goal (fun (x : Lean.MVarId) => #[x]) (Aesop.tryClearS.tacticBuilder goal fvarId) do let a ← goal.tryClear fvarId pure (some a)

def Aesop.tryClearS.tacticBuilder (goal : Lean.MVarId) (fvarId : Lean.FVarId) : Lean.MVarId → Aesop.Script.TacticBuilder

Equations

• Aesop.tryClearS.tacticBuilder goal fvarId x = Aesop.Script.TacticBuilder.clear goal #[fvarId]

def Aesop.tryClearManyS (goal : Lean.MVarId) (fvarIds : Array Lean.FVarId) : Aesop.ScriptM (Lean.MVarId × Array Lean.FVarId)

Equations

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

def Aesop.tryClearManyS.tacticBuilder (goal : Lean.MVarId) : Lean.MVarId × Array Lean.FVarId → Aesop.Script.TacticBuilder

Equations

• Aesop.tryClearManyS.tacticBuilder goal x = match x with | (fst, fvarIds) => Aesop.Script.TacticBuilder.clear goal fvarIds

def Aesop.tryCasesS (goal : Lean.MVarId) (fvarId : Lean.FVarId) (ctorNames : Array Aesop.CtorNames) : Aesop.ScriptM (Option (Array Lean.Meta.CasesSubgoal))

Equations

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

def Aesop.tryCasesS.getUnusedCtorNames (ctorNames : Array Aesop.CtorNames) (lctx : Lean.LocalContext) : Array Aesop.CtorNames

Equations

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

def Aesop.renameInaccessibleFVarsS (goal : Lean.MVarId) : Aesop.ScriptM (Lean.MVarId × Array Lean.FVarId)

Equations

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

def Aesop.renameInaccessibleFVarsS.tacticBuilder : Lean.MVarId × Array Lean.FVarId → Aesop.Script.TacticBuilder

Equations

• Aesop.renameInaccessibleFVarsS.tacticBuilder x = match x with | (goal, renamedFVars) => Aesop.Script.TacticBuilder.renameInaccessibleFVars goal renamedFVars

def Aesop.unfoldManyStarS (goal : Lean.MVarId) (unfold? : Lean.Name → Option (Option Lean.Name)) : Aesop.ScriptM (Aesop.UnfoldResult Lean.MVarId)

Equations

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

def Aesop.introsS (goal : Lean.MVarId) : Aesop.ScriptM (Lean.MVarId × Array Lean.FVarId)

Equations

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

def Aesop.introsS.tacticBuilder : Lean.MVarId × Array Lean.FVarId → Aesop.Script.TacticBuilder

Equations

• Aesop.introsS.tacticBuilder x = match x with | (postGoal, newFVarIds) => Aesop.Script.TacticBuilder.intros postGoal newFVarIds Lean.Meta.TransparencyMode.default

def Aesop.introsUnfoldingS (goal : Lean.MVarId) (md : Lean.Meta.TransparencyMode) : Aesop.ScriptM (Lean.MVarId × Array Lean.FVarId)

Equations

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

def Aesop.introsUnfoldingS.tacticBuilder (md : Lean.Meta.TransparencyMode) : Lean.MVarId × Array Lean.FVarId → Aesop.Script.TacticBuilder

Equations

• Aesop.introsUnfoldingS.tacticBuilder md x = match x with | (postGoal, newFVarIds) => Aesop.Script.TacticBuilder.intros postGoal newFVarIds md

def Aesop.straightLineExtS (goal : Lean.MVarId) : Aesop.ScriptM Aesop.ExtResult

Equations

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

def Aesop.straightLineExtS.tacticBuilder (r : Aesop.ExtResult) : Aesop.Script.TacticBuilder

Equations

• Aesop.straightLineExtS.tacticBuilder = Aesop.Script.TacticBuilder.extN

def Aesop.tryExactFVarS (goal : Lean.MVarId) (fvarId : Lean.FVarId) (md : Lean.Meta.TransparencyMode) : Aesop.ScriptM Bool

Equations

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

def Aesop.splitTargetS? (goal : Lean.MVarId) : Aesop.ScriptM (Option (Array Lean.MVarId))

Equations

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

def Aesop.splitTargetS?.tacticBuilder : Array Lean.MVarId → Aesop.Script.TacticBuilder

Equations

• Aesop.splitTargetS?.tacticBuilder x = Aesop.Script.TacticBuilder.splitTarget

def Aesop.splitFirstHypothesisS? (goal : Lean.MVarId) : Aesop.ScriptM (Option (Array Lean.MVarId))

Equations

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

def Aesop.splitFirstHypothesisS?.tacticBuilder (goal : Lean.MVarId) : Array Lean.MVarId × Lean.FVarId → Aesop.Script.TacticBuilder

Equations

• Aesop.splitFirstHypothesisS?.tacticBuilder goal x = match x with | (fst, fvarId) => Aesop.Script.TacticBuilder.splitAt goal fvarId