HoistSeq (hax-engine.Hax_engine.Side_effect_utils.MakeSI.Hoist.HoistSeq)

val let* : 
  'a Hax_engine.Prelude.Option.t ->
  ('a -> 'b Hax_engine.Prelude.Option.t) ->
  'b Hax_engine.Prelude.Option.t

val many : 
  CollectContext.t ->
  (expr * t) Prelude.list ->
  (expr Prelude.list -> t -> expr * t) ->
  expr * t

val err_hoist_invariant : Span.t -> Prelude.string -> 'r

val one : CollectContext.t -> (expr * t) -> (expr -> t -> expr * t) -> expr * t