VCGen Planner Core #
Shared planning infrastructure for the unary and relational VCGen tactics.
@[implicit_reducible]
def
OracleComp.ProgramLogic.timeNs
{m : Type → Type}
{α : Type}
[Monad m]
[MonadLiftT BaseIO m]
(k : m α)
:
Instances For
def
OracleComp.ProgramLogic.withVCGenTiming
{α : Type}
(add : UInt64 → BaseIO Unit)
(k : Lean.Elab.Tactic.TacticM α)
:
Instances For
Instances For
Instances For
Instances For
def
OracleComp.ProgramLogic.withVCGenProbPlannerTiming
{α : Type}
(k : Lean.Elab.Tactic.TacticM α)
:
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
def
OracleComp.ProgramLogic.withVCGenRunTiming
{α : Type}
(label : String)
(k : Lean.Elab.Tactic.TacticM α)
:
Instances For
- label : String
- replayText : String
- run : Lean.Elab.Tactic.TacticM Bool
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
def
OracleComp.ProgramLogic.renderPlannedStepPreview
(step : PlannedStep)
(preview : PreviewResult)
:
Instances For
def
OracleComp.ProgramLogic.attachPlannerChoiceNotes
(step : PlannedStep)
(preview : PreviewResult)
(alternatives : Array String)
:
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Check if a goal is an equality with probability expressions on both sides.
Instances For
Instances For
Instances For
def
OracleComp.ProgramLogic.runBoundedPasses
(label : String)
(step : Lean.Elab.Tactic.TacticM Bool)
:
Instances For
def
OracleComp.ProgramLogic.runBoundedPassesCollect
{α : Type}
(label : String)
(step : Lean.Elab.Tactic.TacticM (Array α))
: