def
EvalAuto.processHeaderEnsuring
(header : Lean.TSyntax `Lean.Parser.Module.header)
(opts : Lean.Options)
(messages : Lean.MessageLog)
(inputCtx : Lean.Parser.InputContext)
(trustLevel : UInt32 := 0)
(leakEnv : Bool := false)
(ensuring : Array Lean.Import := #[])
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
EvalAuto.runWithEffectOfCommandsCore
{α : Type}
(cnt? : Option Nat)
(action :
Lean.Elab.Frontend.Context → Lean.Elab.Frontend.State → Lean.Elab.Frontend.State → Lean.ConstantInfo → IO (Option α))
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
EvalAuto.runWithEffectOfCommands
{α : Type}
(input fileName : String)
(cnt? : Option Nat)
(action :
Lean.Elab.Frontend.Context → Lean.Elab.Frontend.State → Lean.Elab.Frontend.State → Lean.ConstantInfo → IO (Option α))
:
Lean.CoreM (Array α)
Given a Lean4 file fileName with content input consisting of
a header and a series of commands, first parse the header. Then,
for each command cmd, record the states st₁, st₂ before and
after executing the command, and run action on the ConstantInfos produced
by cmd, together with st₁, st₂ and the InputContext.
An additional cnt? can be supplied to control termination.
When the number of times action returns .some _ reaches cnt?,
the procedure is terminated.
Equations
- One or more equations did not get rendered due to their size.