Hoist (hax-engine.Hax_engine.Side_effect

Parameters

module F : 
  Features.T
    with type monadic_binding = Features.Off.monadic_binding
     and type for_index_loop = Features.Off.for_index_loop

module FA = F

module FB : sig ... end

module UA : sig ... end

module UB : sig ... end

module A : sig ... end

module B : sig ... end

module S : sig ... end

val dmutability : 
  Span.t ->
  (Span.t -> 'a -> 'b) ->
  'a0 Hax_engine__Ast.mutability ->
  'b0 Hax_engine__Ast.mutability

val dsafety_kind : Span.t -> A.safety_kind -> B.safety_kind

module ID : sig ... end

val dexpr : A.expr -> B.expr

val dgeneric_param : 'a -> A.generic_param -> B.generic_param

val dgeneric_constraint : 
  Span.t ->
  A.generic_constraint ->
  B.generic_constraint

val dgenerics : Span.t -> A.generics -> B.generics

val dparam : Span.t -> A.param -> B.param

val dvariant : Span.t -> A.variant -> B.variant

val dtrait_item' : Span.t -> A.trait_item' -> B.trait_item'

val dtrait_item : A.trait_item -> B.trait_item

val dimpl_item' : Span.t -> A.impl_item' -> B.impl_item'

val dimpl_item : A.impl_item -> B.impl_item

val ditem : A.item -> B.item Prelude.list

val ditem_unwrapped : A.item -> B.item Prelude.list

val ditem' : Span.t -> Hax_engine__Ast.Make(F).item' -> B.item'

val ditems : 
  A.item Hax_engine.Prelude.List.t ->
  B.item Hax_engine.Prelude.List.t

val metadata : Phase_utils.Metadata.t