This file enables us to transverse tactics and test for conditions.

References

The content of this file is based on the following sources (released under the Apache 2.0 license).

• https://github.com/dwrensha/tryAtEachStep/blob/main/tryAtEachStep.lean
• https://github.com/lean-dojo/LeanDojo/blob/main/src/lean_dojo/data_extraction/ExtractData.lean

Modifications have been made to the original content of these files here.

See also:

• https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Memory.20increase.20in.20loops.2E

partial def transverseTactics.processCommands : Lean.Elab.Frontend.FrontendM (List (Lean.Environment × Lean.Elab.InfoState))

Takes in a file and returns the infostates of commands and the corresponding environment before the command is processed.

def transverseTactics.visitInfo (file : System.FilePath) (env : Lean.Environment) (visitTacticInfo : System.FilePath → Lean.Elab.ContextInfo → Lean.Elab.TacticInfo → Lean.MetaM Unit) (ci : Lean.Elab.ContextInfo) (info : Lean.Elab.Info) (acc : List (IO Unit)) : List (IO Unit)

Tests if a given info is ofTacticInfo and if so runs visitTacticInfo.

Equations

• One or more equations did not get rendered due to their size.
• transverseTactics.visitInfo file env visitTacticInfo ci info acc = acc

def transverseTactics.traverseForest (file : System.FilePath) (visitTacticInfo : System.FilePath → Lean.Elab.ContextInfo → Lean.Elab.TacticInfo → Lean.MetaM Unit) (steps : List (Lean.Environment × Lean.Elab.InfoState)) : List (IO Unit)

Applies visitInfo to each node of the info trees.

Equations

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

unsafe def transverseTactics (file : System.FilePath) (visitTacticInfo : System.FilePath → Lean.Elab.ContextInfo → Lean.Elab.TacticInfo → Lean.MetaM Unit) : IO Unit

Applies visitTacticInfo to each tactic in a file.

Equations

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