Basic operations on MLList

These functions can be upstreamed to Std when convenient.

def MLList.singletonM {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (x : m α) : MLList m α

Construct a singleton monadic lazy list from a single monadic value.

Equations

• MLList.singletonM x = MLList.squash fun (x_1 : Unit) => do let __do_lift ← x pure (MLList.cons __do_lift MLList.nil)

def MLList.singleton {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (x : α) : MLList m α

Construct a singleton monadic lazy list from a single value.

Equations

• MLList.singleton x = MLList.singletonM (pure x)