def Aesop.Script.Tactic.skip : 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) : 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) : 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) : TacticBuilder

Equations

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

def Aesop.Script.TacticBuilder.replace (preGoal postGoal : Lean.MVarId) (fvarId : Lean.FVarId) (type proof : Lean.Expr) : 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) : 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) : 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 CtorNames) : 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 : CtorNames) : 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 CtorNames) : 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) : TacticBuilder

Equations

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

def Aesop.Script.TacticBuilder.unfold (usedDecls : Array Lean.Name) (aesopUnfold : Bool) : TacticBuilder

Equations

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

def Aesop.Script.TacticBuilder.unfoldAt (goal : Lean.MVarId) (fvarId : Lean.FVarId) (usedDecls : Array Lean.Name) (aesopUnfold : Bool) : TacticBuilder

Equations

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

def Aesop.Script.TacticBuilder.extN (r : ExtResult) : 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) : TacticBuilder

Equations

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

def Aesop.Script.TacticBuilder.simpAllOrSimpAtStar (simpAll : Bool) (inGoal : Lean.MVarId) (configStx? : Option Lean.Term) (usedTheorems : Lean.Meta.Simp.UsedSimps) : 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) : TacticBuilder

Equations

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

def Aesop.Script.TacticBuilder.splitTarget : 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) : 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) : TacticBuilder

Equations

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

def Aesop.Script.TacticBuilder.substFVars' (fvarUserNames : Array Lean.Name) : 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) : 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 → 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) : 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 → Script.TacticBuilder

Equations

• Aesop.applyS.tacticBuilder goal e none md x✝ = Aesop.Script.TacticBuilder.apply goal e md
• Aesop.applyS.tacticBuilder goal e (some cfg) md x✝ = Aesop.Script.TacticBuilder.applyStx cfg md

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

Equations

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

def Aesop.replaceFVarS.tacticBuilder (goal : Lean.MVarId) (fvarId : Lean.FVarId) (type proof : Lean.Expr) : Lean.MVarId × Lean.FVarId × Bool → 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) : 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 → Script.TacticBuilder

Equations

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

def Aesop.tryClearS (goal : Lean.MVarId) (fvarId : Lean.FVarId) : 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 → 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) : 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 → Script.TacticBuilder

Equations

• Aesop.tryClearManyS.tacticBuilder goal (g, fvarIds) = Aesop.Script.TacticBuilder.clear goal fvarIds

def Aesop.tryCasesS (goal : Lean.MVarId) (fvarId : Lean.FVarId) (ctorNames : Array CtorNames) : 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 CtorNames) (lctx : Lean.LocalContext) : Array CtorNames

Equations

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

def Aesop.renameInaccessibleFVarsS (goal : Lean.MVarId) : 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 → Script.TacticBuilder

Equations

• Aesop.renameInaccessibleFVarsS.tacticBuilder (g, fvarIds) = Aesop.Script.TacticBuilder.renameInaccessibleFVars g fvarIds

def Aesop.unfoldManyTargetS (unfold? : Lean.Name → Option (Option Lean.Name)) (goal : Lean.MVarId) : ScriptM (Option (Lean.MVarId × Array Lean.Name))

Equations

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

def Aesop.unfoldManyAtS (unfold? : Lean.Name → Option (Option Lean.Name)) (goal : Lean.MVarId) (fvarId : Lean.FVarId) : ScriptM (Option (Lean.MVarId × Array Lean.Name))

Equations

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

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

Equations

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

def Aesop.introsS (goal : Lean.MVarId) : 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 → Script.TacticBuilder

Equations

• Aesop.introsS.tacticBuilder (g, fvarIds) = Aesop.Script.TacticBuilder.intros g fvarIds Lean.Meta.TransparencyMode.default

def Aesop.introsUnfoldingS (goal : Lean.MVarId) (md : Lean.Meta.TransparencyMode) : 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 → Script.TacticBuilder

Equations

• Aesop.introsUnfoldingS.tacticBuilder md (g, fvarIds) = Aesop.Script.TacticBuilder.intros g fvarIds md

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

Equations

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

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

Equations

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

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

Equations

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

def Aesop.splitTargetS? (goal : Lean.MVarId) : 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 → Script.TacticBuilder

Equations

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

def Aesop.splitFirstHypothesisS? (goal : Lean.MVarId) : 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 → Script.TacticBuilder

Equations

• Aesop.splitFirstHypothesisS?.tacticBuilder goal (fst, fvarId) = Aesop.Script.TacticBuilder.splitAt goal fvarId