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.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.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.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.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.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.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.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.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.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.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.straightLineExtS (goal : Lean.MVarId) : ScriptM ExtResult

Equations

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

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.splitFirstHypothesisS? (goal : Lean.MVarId) : ScriptM (Option (Array Lean.MVarId))

Equations

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