structure Aesop.GoalWithMVars : Type

• goal : Lean.MVarId
• mvars : Lean.HashSet Lean.MVarId

instance Aesop.instInhabitedGoalWithMVars : Inhabited Aesop.GoalWithMVars

Equations

• Aesop.instInhabitedGoalWithMVars = { default := { goal := default, mvars := default } }

instance Aesop.instReprGoalWithMVars : Repr Aesop.GoalWithMVars

Equations

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

instance Aesop.instBEqGoalWithMVars : BEq Aesop.GoalWithMVars

Equations

• Aesop.instBEqGoalWithMVars = { beq := fun (g₁ g₂ : Aesop.GoalWithMVars) => g₁.goal == g₂.goal }

def Aesop.GoalWithMVars.ofMVarId (goal : Lean.MVarId) : Lean.MetaM Aesop.GoalWithMVars

Equations

• Aesop.GoalWithMVars.ofMVarId goal = do let __do_lift ← Lean.MVarId.getMVarDependencies goal false pure { goal := goal, mvars := __do_lift }

def Aesop.UnstructuredScriptBuilder (m : Type → Type u_1) : Type u_1

Equations

• Aesop.UnstructuredScriptBuilder m = m (Array Lean.Syntax.Tactic)

@[inline]

def Aesop.UnstructuredScriptBuilder.run {m : Type → Type} (b : Aesop.UnstructuredScriptBuilder m) : m (Array Lean.Syntax.Tactic)

Equations

• Aesop.UnstructuredScriptBuilder.run b = b

@[inline]

def Aesop.UnstructuredScriptBuilder.ofTactics {m : Type → Type} [Monad m] (ts : m (Array Lean.Syntax.Tactic)) : Aesop.UnstructuredScriptBuilder m

Equations

• Aesop.UnstructuredScriptBuilder.ofTactics ts = do let __do_lift ← ts pure __do_lift

@[inline]

def Aesop.UnstructuredScriptBuilder.ofTactic {m : Type → Type} [Monad m] (t : m Lean.Syntax.Tactic) : Aesop.UnstructuredScriptBuilder m

Equations

• Aesop.UnstructuredScriptBuilder.ofTactic t = do let __do_lift ← t pure #[__do_lift]

@[inline]

def Aesop.UnstructuredScriptBuilder.seq {m : Type → Type} [Monad m] (b₁ : Aesop.UnstructuredScriptBuilder m) (b₂ : Aesop.UnstructuredScriptBuilder m) : Aesop.UnstructuredScriptBuilder m

Equations

• Aesop.UnstructuredScriptBuilder.seq b₁ b₂ = do let __do_lift ← Aesop.UnstructuredScriptBuilder.run b₁ let __do_lift_1 ← Aesop.UnstructuredScriptBuilder.run b₂ pure (__do_lift ++ __do_lift_1)

@[inline]

def Aesop.UnstructuredScriptBuilder.focusAndDoneEach {m : Type → Type} [Monad m] [Lean.MonadQuotation m] [Lean.MonadError m] (bs : Array (Aesop.UnstructuredScriptBuilder m)) : Aesop.UnstructuredScriptBuilder m

Equations

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

@[inline]

def Aesop.UnstructuredScriptBuilder.seqFocusAndDone {m : Type → Type} [Monad m] [Lean.MonadQuotation m] [Lean.MonadError m] (b : Aesop.UnstructuredScriptBuilder m) (bs : Array (Aesop.UnstructuredScriptBuilder m)) : Aesop.UnstructuredScriptBuilder m

Equations

• Aesop.UnstructuredScriptBuilder.seqFocusAndDone b bs = Aesop.UnstructuredScriptBuilder.seq b (Aesop.UnstructuredScriptBuilder.focusAndDoneEach bs)

@[inline]

def Aesop.UnstructuredScriptBuilder.seqFocus {m : Type → Type} [Monad m] [Lean.MonadQuotation m] [Lean.MonadError m] (b : Aesop.UnstructuredScriptBuilder m) (bs : Array (Aesop.UnstructuredScriptBuilder m)) : Aesop.UnstructuredScriptBuilder m

Equations

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

@[inline]

def Aesop.UnstructuredScriptBuilder.id {m : Type → Type} [Monad m] : Aesop.UnstructuredScriptBuilder m

Equations

• Aesop.UnstructuredScriptBuilder.id = pure #[]

instance Aesop.UnstructuredScriptBuilder.instInhabitedUnstructuredScriptBuilder {m : Type → Type} [Pure m] : Inhabited (Aesop.UnstructuredScriptBuilder m)

Equations

• Aesop.UnstructuredScriptBuilder.instInhabitedUnstructuredScriptBuilder = { default := pure #[] }

structure Aesop.StructuredScriptBuilder (m : Type → Type) : Type

• subgoals : Nat
• elim : Subarray (Aesop.UnstructuredScriptBuilder m) → Aesop.UnstructuredScriptBuilder m

@[inline]

def Aesop.StructuredScriptBuilder.run {m : Type → Type} (b : Aesop.StructuredScriptBuilder m) : m (Array Lean.Syntax.Tactic)

Equations

• Aesop.StructuredScriptBuilder.run b = b.elim (Array.toSubarray #[] 0)

def Aesop.StructuredScriptBuilder.id {m : Type → Type} [Monad m] [Lean.MonadError m] : Aesop.StructuredScriptBuilder m

Equations

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

def Aesop.StructuredScriptBuilder.ofTactics {m : Type → Type} [Monad m] [Lean.MonadQuotation m] [Lean.MonadError m] (subgoals : Nat) (ts : m (Array Lean.Syntax.Tactic)) : Aesop.StructuredScriptBuilder m

Equations

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

@[inline]

def Aesop.StructuredScriptBuilder.ofUnstructuredScriptBuilder {m : Type → Type} [Monad m] [Lean.MonadQuotation m] [Lean.MonadError m] (subgoals : Nat) (b : Aesop.UnstructuredScriptBuilder m) : Aesop.StructuredScriptBuilder m

Equations

• Aesop.StructuredScriptBuilder.ofUnstructuredScriptBuilder subgoals b = Aesop.StructuredScriptBuilder.ofTactics subgoals b

@[inline]

def Aesop.StructuredScriptBuilder.ofTactic {m : Type → Type} [Monad m] [Lean.MonadQuotation m] [Lean.MonadError m] (subgoals : Nat) (t : m Lean.Syntax.Tactic) : Aesop.StructuredScriptBuilder m

Equations

• Aesop.StructuredScriptBuilder.ofTactic subgoals t = Aesop.StructuredScriptBuilder.ofTactics subgoals do let __do_lift ← t pure #[__do_lift]

@[inline]

def Aesop.StructuredScriptBuilder.done {m : Type → Type} [Monad m] [Lean.MonadQuotation m] [Lean.MonadError m] : Aesop.StructuredScriptBuilder m

Equations

• Aesop.StructuredScriptBuilder.done = Aesop.StructuredScriptBuilder.ofTactics 0 (pure #[])

instance Aesop.StructuredScriptBuilder.instInhabitedStructuredScriptBuilder {m : Type → Type} [Monad m] [Lean.MonadError m] : Inhabited (Aesop.StructuredScriptBuilder m)

Equations

• Aesop.StructuredScriptBuilder.instInhabitedStructuredScriptBuilder = { default := Aesop.StructuredScriptBuilder.id }

def Aesop.StructuredScriptBuilder.error {m : Type → Type} [Monad m] [Lean.MonadError m] (msg : Lean.MessageData) : Aesop.StructuredScriptBuilder m

Equations

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

def Aesop.StructuredScriptBuilder.seq {m : Type → Type} [Monad m] [Lean.MonadError m] (b : Aesop.StructuredScriptBuilder m) (bs : Array (Aesop.StructuredScriptBuilder m)) : Aesop.StructuredScriptBuilder m

Equations

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

structure Aesop.ScriptBuilder (m : Type → Type) : Type

• unstructured : Aesop.UnstructuredScriptBuilder m
• structured : Aesop.StructuredScriptBuilder m

instance Aesop.instInhabitedScriptBuilder {m : Type → Type} [Monad m] [Lean.MonadError m] [Pure m] : Inhabited (Aesop.ScriptBuilder m)

Equations

• Aesop.instInhabitedScriptBuilder = { default := { unstructured := default, structured := default } }

def Aesop.ScriptBuilder.id {m : Type → Type} [Monad m] [Lean.MonadError m] : Aesop.ScriptBuilder m

Equations

• Aesop.ScriptBuilder.id = { unstructured := Aesop.UnstructuredScriptBuilder.id, structured := Aesop.StructuredScriptBuilder.id }

def Aesop.ScriptBuilder.ofTactics {m : Type → Type} [Monad m] [Lean.MonadQuotation m] [Lean.MonadError m] (subgoals : Nat) (ts : m (Array Lean.Syntax.Tactic)) : Aesop.ScriptBuilder m

Equations

• Aesop.ScriptBuilder.ofTactics subgoals ts = { unstructured := Aesop.UnstructuredScriptBuilder.ofTactics ts, structured := Aesop.StructuredScriptBuilder.ofTactics subgoals ts }

@[inline]

def Aesop.ScriptBuilder.ofUnstructuredScriptBuilder {m : Type → Type} [Monad m] [Lean.MonadQuotation m] [Lean.MonadError m] (subgoals : Nat) (b : Aesop.UnstructuredScriptBuilder m) : Aesop.ScriptBuilder m

Equations

• Aesop.ScriptBuilder.ofUnstructuredScriptBuilder subgoals b = Aesop.ScriptBuilder.ofTactics subgoals b

def Aesop.ScriptBuilder.ofTactic {m : Type → Type} [Monad m] [Lean.MonadQuotation m] [Lean.MonadError m] (subgoals : Nat) (t : m Lean.Syntax.Tactic) : Aesop.ScriptBuilder m

Equations

• Aesop.ScriptBuilder.ofTactic subgoals t = { unstructured := Aesop.UnstructuredScriptBuilder.ofTactic t, structured := Aesop.StructuredScriptBuilder.ofTactic subgoals t }

def Aesop.ScriptBuilder.seq {m : Type → Type} [Monad m] [Lean.MonadQuotation m] [Lean.MonadError m] (b : Aesop.ScriptBuilder m) (bs : Array (Aesop.ScriptBuilder m)) : Aesop.ScriptBuilder m

Equations

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

def Aesop.ScriptBuilder.assertHypotheses (goal : Lean.MVarId) (hs : Array Lean.Meta.Hypothesis) : Aesop.ScriptBuilder Lean.MetaM

Equations

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

def Aesop.ScriptBuilder.clear (goal : Lean.MVarId) (fvarIds : Array Lean.FVarId) : Aesop.ScriptBuilder Lean.MetaM

Equations

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

def Aesop.ScriptBuilder.unhygienicAesopCases (goal : Lean.MVarId) (fvarId : Lean.FVarId) (subgoals : Nat) : Aesop.ScriptBuilder Lean.MetaM

Equations

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

def Aesop.ScriptBuilder.renameInaccessibleFVars (goal : Lean.MVarId) (renamedFVars : Array Lean.FVarId) : Aesop.ScriptBuilder Lean.MetaM

Equations

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

def Aesop.ScriptBuilder.unfoldManyStar (usedDecls : Lean.HashSet Lean.Name) : Aesop.ScriptBuilder Lean.MetaM

Equations

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

def Aesop.ScriptBuilder.unhygienicExt (subgoals : Nat) : Aesop.ScriptBuilder Lean.MetaM

Equations

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

@[always_inline]

def Aesop.ScriptBuilder.withPrefix {m : Type → Type} [Monad m] [Lean.MonadQuotation m] [Lean.MonadError m] (f : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq → m (Array (Lean.TSyntax `tactic))) (b : Aesop.ScriptBuilder m) : Aesop.ScriptBuilder m

Equations

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

def Aesop.ScriptBuilder.withTransparency {m : Type → Type} [Monad m] [Lean.MonadQuotation m] [Lean.MonadError m] (md : Lean.Meta.TransparencyMode) (b : Aesop.ScriptBuilder m) : Aesop.ScriptBuilder m

Equations

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

def Aesop.ScriptBuilder.withAllTransparency {m : Type → Type} [Monad m] [Lean.MonadQuotation m] [Lean.MonadError m] (md : Lean.Meta.TransparencyMode) (b : Aesop.ScriptBuilder m) : Aesop.ScriptBuilder m

Equations

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

@[inline, reducible]

abbrev Aesop.RuleTacScriptBuilder : Type

Equations

• Aesop.RuleTacScriptBuilder = Aesop.ScriptBuilder Lean.MetaM

@[always_inline]

def Aesop.mkScriptBuilder? (generateScript : Bool) (builder : Aesop.ScriptBuilder Lean.MetaM) : Option (Aesop.ScriptBuilder Lean.MetaM)

Equations

• Aesop.mkScriptBuilder? generateScript builder = if generateScript = true then some builder else none

def Aesop.assertHypothesesWithScript (goal : Lean.MVarId) (hs : Array Lean.Meta.Hypothesis) (generateScript : Bool) : Lean.MetaM (Array Lean.FVarId × Lean.MVarId × Option (Aesop.ScriptBuilder Lean.MetaM))

Equations

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

def Aesop.clearWithScript (goal : Lean.MVarId) (fvarId : Lean.FVarId) (generateScript : Bool) : Lean.MetaM (Lean.MVarId × Option (Aesop.ScriptBuilder Lean.MetaM))

Equations

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

def Aesop.tryClearWithScript (goal : Lean.MVarId) (fvarId : Lean.FVarId) (generateScript : Bool) : Lean.MetaM (Lean.MVarId × Option (Aesop.ScriptBuilder Lean.MetaM))

Equations

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

def Aesop.tryClearManyWithScript (goal : Lean.MVarId) (fvarIds : Array Lean.FVarId) (generateScript : Bool) : Lean.MetaM (Lean.MVarId × Array Lean.FVarId × Option (Aesop.ScriptBuilder Lean.MetaM))

Equations

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

def Aesop.unhygienicCasesWithScript (goal : Lean.MVarId) (fvarId : Lean.FVarId) (generateScript : Bool) : Lean.MetaM (Array Lean.Meta.CasesSubgoal × Option (Aesop.ScriptBuilder Lean.MetaM))

Equations

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

def Aesop.renameInaccessibleFVarsWithScript (goal : Lean.MVarId) (generateScript : Bool) : Lean.MetaM (Lean.MVarId × Array Lean.FVarId × Option (Aesop.ScriptBuilder Lean.MetaM))

Equations

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

def Aesop.unfoldManyStarWithScript (goal : Lean.MVarId) (unfold? : Lean.Name → Option (Option Lean.Name)) (generateScript : Bool) : Lean.MetaM (Aesop.UnfoldResult Lean.MVarId × Option (Aesop.ScriptBuilder Lean.MetaM))

Equations

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

structure Aesop.TacticState : Type

• visibleGoals : Array Aesop.GoalWithMVars
• invisibleGoals : Lean.HashSet Lean.MVarId

instance Aesop.instInhabitedTacticState : Inhabited Aesop.TacticState

Equations

• Aesop.instInhabitedTacticState = { default := { visibleGoals := default, invisibleGoals := default } }

def Aesop.TacticState.getVisibleGoalIndex? (ts : Aesop.TacticState) (goal : Lean.MVarId) : Option Nat

Equations

• Aesop.TacticState.getVisibleGoalIndex? ts goal = Array.findIdx? ts.visibleGoals fun (x : Aesop.GoalWithMVars) => x.goal == goal

def Aesop.TacticState.getVisibleGoalIndex {m : Type → Type} [Monad m] [Lean.MonadError m] (ts : Aesop.TacticState) (goal : Lean.MVarId) : m Nat

Equations

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

def Aesop.TacticState.getMainGoal? (ts : Aesop.TacticState) : Option Lean.MVarId

Equations

• Aesop.TacticState.getMainGoal? ts = Option.map (fun (x : Aesop.GoalWithMVars) => x.goal) ts.visibleGoals[0]?

def Aesop.TacticState.hasNoVisibleGoals (ts : Aesop.TacticState) : Bool

Equations

• Aesop.TacticState.hasNoVisibleGoals ts = Array.isEmpty ts.visibleGoals

def Aesop.TacticState.hasSingleVisibleGoal (ts : Aesop.TacticState) : Bool

Equations

• Aesop.TacticState.hasSingleVisibleGoal ts = (Array.size ts.visibleGoals == 1)

def Aesop.TacticState.visibleGoalsHaveMVars (ts : Aesop.TacticState) : Bool

Equations

• Aesop.TacticState.visibleGoalsHaveMVars ts = Array.any ts.visibleGoals (fun (g : Aesop.GoalWithMVars) => !Lean.HashSet.isEmpty g.mvars) 0

def Aesop.TacticState.eraseSolvedGoals (ts : Aesop.TacticState) (mctx : Lean.MetavarContext) : Aesop.TacticState

Equations

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

def Aesop.TacticState.applyTactic {m : Type → Type} [Monad m] [Lean.MonadError m] (ts : Aesop.TacticState) (inGoal : Lean.MVarId) (outGoals : Array Aesop.GoalWithMVars) (postMCtx : Lean.MetavarContext) : m Aesop.TacticState

Equations

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

def Aesop.TacticState.focus {m : Type → Type} [Monad m] [Lean.MonadError m] (ts : Aesop.TacticState) (goal : Lean.MVarId) : m Aesop.TacticState

Equations

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

@[always_inline]

def Aesop.TacticState.onGoalM {m : Type → Type} [Monad m] [Lean.MonadError m] {α : Type} (ts : Aesop.TacticState) (g : Lean.MVarId) (f : Aesop.TacticState → m (α × Aesop.TacticState)) : m (α × Aesop.TacticState)

Equations

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

structure Aesop.TacticInvocation : Type

• preState : Lean.Meta.SavedState
• preGoal : Lean.MVarId
• tacticSeq : Array Lean.Syntax.Tactic
• postGoals : Array Aesop.GoalWithMVars
• postState : Lean.Meta.SavedState

instance Aesop.instNonemptyTacticInvocation : Nonempty Aesop.TacticInvocation

Equations

• Aesop.instNonemptyTacticInvocation = (_ : Nonempty Aesop.TacticInvocation)

def Aesop.TacticState.applyTacticInvocation {m : Type → Type} [Monad m] [Lean.MonadError m] (tacticState : Aesop.TacticState) (ti : Aesop.TacticInvocation) : m Aesop.TacticState

Equations

• Aesop.TacticState.applyTacticInvocation tacticState ti = Aesop.TacticState.applyTactic tacticState ti.preGoal ti.postGoals ti.postState.meta.mctx

def Aesop.TacticInvocation.noop (preGoal : Lean.MVarId) (postGoal : Aesop.GoalWithMVars) (preState : Lean.Meta.SavedState) (postState : Lean.Meta.SavedState) : Aesop.TacticInvocation

Equations

• Aesop.TacticInvocation.noop preGoal postGoal preState postState = { preState := preState, preGoal := preGoal, tacticSeq := #[], postGoals := #[postGoal], postState := postState }

def Aesop.TacticInvocation.render {m : Type → Type} [Monad m] [Lean.MonadQuotation m] [Lean.MonadError m] (acc : Array Lean.Syntax.Tactic) (ti : Aesop.TacticInvocation) (tacticState : Aesop.TacticState) : m (Array Lean.Syntax.Tactic × Aesop.TacticState)

Equations

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

def Aesop.TacticInvocation.validate (ti : Aesop.TacticInvocation) : Lean.MetaM Unit

Equations

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

def Aesop.TacticInvocation.validate.fmtGoals (state : Lean.Meta.SavedState) (goals : Array Lean.MVarId) : Lean.MetaM Lean.MessageData

Equations

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

@[inline, reducible]

abbrev Aesop.UnstructuredScript : Type

Equations

• Aesop.UnstructuredScript = Array Aesop.TacticInvocation

def Aesop.UnstructuredScript.render {m : Type → Type} [Monad m] [Lean.MonadQuotation m] [Lean.MonadError m] (tacticState : Aesop.TacticState) (s : Aesop.UnstructuredScript) : m (Array Lean.Syntax.Tactic)

Equations

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

def Aesop.UnstructuredScript.validate (s : Aesop.UnstructuredScript) : Lean.MetaM Unit

Equations

• Aesop.UnstructuredScript.validate s = Array.forM (fun (x : Aesop.TacticInvocation) => Aesop.TacticInvocation.validate x) s 0 (Array.size s)

inductive Aesop.StructuredScript : Type

• empty: Aesop.StructuredScript
• unstructuredStep: Aesop.TacticInvocation → Aesop.StructuredScript → Aesop.StructuredScript
• solve: Lean.MVarId → Aesop.StructuredScript → Aesop.StructuredScript → Aesop.StructuredScript

instance Aesop.instInhabitedStructuredScript : Inhabited Aesop.StructuredScript

Equations

• Aesop.instInhabitedStructuredScript = { default := Aesop.StructuredScript.empty }

def Aesop.StructuredScript.render {m : Type → Type} [Monad m] [Lean.MonadQuotation m] [Lean.MonadError m] (tacticState : Aesop.TacticState) (script : Aesop.StructuredScript) : m (Array Lean.Syntax.Tactic)

Equations

• Aesop.StructuredScript.render tacticState script = (fun (x : Array Lean.Syntax.Tactic × Aesop.TacticState) => x.fst) <$> Aesop.StructuredScript.render.go #[] tacticState script

def Aesop.StructuredScript.render.go {m : Type → Type} [Monad m] [Lean.MonadQuotation m] [Lean.MonadError m] (script : Array Lean.Syntax.Tactic) (tacticState : Aesop.TacticState) : Aesop.StructuredScript → m (Array Lean.Syntax.Tactic × Aesop.TacticState)

Equations

• One or more equations did not get rendered due to their size.
• Aesop.StructuredScript.render.go script tacticState Aesop.StructuredScript.empty = pure (script, tacticState)

def Aesop.UnstructuredScript.toStructuredScript {m : Type → Type} [Monad m] [Lean.MonadError m] (tacticState : Aesop.TacticState) (script : Aesop.UnstructuredScript) : m Aesop.StructuredScript

Equations

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

partial def Aesop.UnstructuredScript.toStructuredScript.go {m : Type → Type} [Monad m] [Lean.MonadError m] (steps : Lean.HashMap Lean.MVarId (Nat × Aesop.TacticInvocation)) (tacticState : Aesop.TacticState) : m (Aesop.StructuredScript × Aesop.TacticState)