def replicateG {G : Type} [Monoid G] {M : GradedType G} [GradedMonad M] {g : G} {α : Type} (x : M g α) (n : ℕ) : M (g ^ n) (List.Vector α n)

Run a graded computation n times, collecting results into a vector.

Equations

• replicateG x 0 = gcast ⋯ (gpure List.Vector.nil)
• replicateG x n.succ = gcast ⋯ (x >>=ᵍ fun (h : α) => replicateG x n >>=ᵍ fun (t : List.Vector α n) => gpure (h ::ᵥ t))

def between' {G : Type} [Monoid G] {M : GradedType G} [GradedMonad M] {g gl gr : G} {α β γ : Type} (l : M gl α) (r : M gr β) (c : M g γ) : M (gl * g * gr) (α × γ × β)

Run c between l and r, returning all three results.

Equations

• between' l r c = gcast ⋯ (l >>=ᵍ fun (l' : α) => c >>=ᵍ fun (c' : γ) => r >>=ᵍ fun (r' : β) => gpure (l', c', r'))

def between {G : Type} [Monoid G] {M : GradedType G} [GradedMonad M] {g gl gr : G} {α β γ : Type} (l : M gl α) (r : M gr β) (c : M g γ) : M (gl * g * gr) γ

Run c between l and r, returning only the middle result.

Equations

• between l r c = (fun (x : α × γ × β) => x.2.1) <$>ᵍ between' l r c