Running a Computation Multiple Times

This file defines a function replicate oa n that runs the computation oa a total of n times, returning the result as a list of length n.

Note that while the executions are independent, they may no longer be after calling simulate.

def OracleComp.replicate {ι : Type u_1} {spec : OracleSpec ι} {α : Type v} (n : ℕ) (oa : OracleComp spec α) : OracleComp spec (List α)

Run the computation oa repeatedly n times to get a vector of n results.

def OracleComp.replicateTR {ι : Type u_1} {spec : OracleSpec ι} {α : Type v} (n : ℕ) (oa : OracleComp spec α) : OracleComp spec (List α)

@[simp]

theorem OracleComp.replicate_zero {ι : Type u_2} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) : replicate 0 oa = pure []

@[simp]

theorem OracleComp.replicateTR_zero {ι : Type u_2} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) : replicate 0 oa = pure []

@[simp]

theorem OracleComp.replicate_succ {ι : Type u_2} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) (n : ℕ) : replicate (n + 1) oa = List.cons <$> oa <*> replicate n oa

@[simp]

theorem OracleComp.replicate_pure {ι : Type u_2} {spec : OracleSpec ι} {α : Type v} (n : ℕ) (x : α) : replicate n (pure x) = pure (List.replicate n x)