Reducers (hax-engine.Hax_engine.Ast

val collect_local_idents : 
  < visit_F__arbitrary_lhs : 
    unit ->
    F.arbitrary_lhs ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__as_pattern : 
    unit ->
    F.as_pattern ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__block : 
    unit ->
    F.block ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__break : 
    unit ->
    F.break ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__construct_base : 
    unit ->
    F.construct_base ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__continue : 
    unit ->
    F.continue ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__dyn : 
    unit ->
    F.dyn ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__early_exit : 
    unit ->
    F.early_exit ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__fold_like_loop : 
    unit ->
    F.fold_like_loop ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__for_index_loop : 
    unit ->
    F.for_index_loop ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__for_loop : 
    unit ->
    F.for_loop ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__lifetime : 
    unit ->
    F.lifetime ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__loop : 
    unit ->
    F.loop ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__macro : 
    unit ->
    F.macro ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__match_guard : 
    unit ->
    F.match_guard ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__monadic_action : 
    unit ->
    F.monadic_action ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__monadic_binding : 
    unit ->
    F.monadic_binding ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__mutable_pointer : 
    unit ->
    F.mutable_pointer ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__mutable_reference : 
    unit ->
    F.mutable_reference ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__mutable_variable : 
    unit ->
    F.mutable_variable ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__nontrivial_lhs : 
    unit ->
    F.nontrivial_lhs ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__question_mark : 
    unit ->
    F.question_mark ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__quote : 
    unit ->
    F.quote ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__raw_pointer : 
    unit ->
    F.raw_pointer ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__reference : 
    unit ->
    F.reference ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__slice : 
    unit ->
    F.slice ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__state_passing_loop : 
    unit ->
    F.state_passing_loop ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__trait_item_default : 
    unit ->
    F.trait_item_default ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__unsafe : 
    unit ->
    F.unsafe ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__while_loop : 
    unit ->
    F.while_loop ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_Local_ident__t : 
    unit ->
    Local_ident.t ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_arm : 
    unit ->
    Hax_engine__Ast.Make(F).arm ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_arm' : 
    unit ->
    Hax_engine__Ast.Make(F).arm' ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_attr : 
    unit ->
    Ast.attr ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_attrs : 
    unit ->
    Ast.attrs ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_binding_mode : 
    unit ->
    Hax_engine__Ast.Make(F).binding_mode ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_bool : 
    unit ->
    Base.bool ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_borrow_kind : 
    unit ->
    Hax_engine__Ast.Make(F).borrow_kind ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_cf_kind : 
    unit ->
    Hax_engine__Ast.Make(F).cf_kind ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_char : 
    unit ->
    Base.char ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_concrete_ident : 
    unit ->
    Ast.concrete_ident ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_dyn_trait_goal : 
    unit ->
    Hax_engine__Ast.Make(F).dyn_trait_goal ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_expr : 
    unit ->
    Hax_engine__Ast.Make(F).expr ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_expr' : 
    unit ->
    Hax_engine__Ast.Make(F).expr' ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_field_pat : 
    unit ->
    Hax_engine__Ast.Make(F).field_pat ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_float_kind : 
    unit ->
    Ast.float_kind ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_generic_constraint : 
    unit ->
    Hax_engine__Ast.Make(F).generic_constraint ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_generic_param : 
    unit ->
    Hax_engine__Ast.Make(F).generic_param ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_generic_param_kind : 
    unit ->
    Hax_engine__Ast.Make(F).generic_param_kind ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_generic_value : 
    unit ->
    Hax_engine__Ast.Make(F).generic_value ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_generics : 
    unit ->
    Hax_engine__Ast.Make(F).generics ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_global_ident : 
    unit ->
    Ast.global_ident ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_guard : 
    unit ->
    Hax_engine__Ast.Make(F).guard ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_guard' : 
    unit ->
    Hax_engine__Ast.Make(F).guard' ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_impl_expr : 
    unit ->
    Hax_engine__Ast.Make(F).impl_expr ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_impl_expr_kind : 
    unit ->
    Hax_engine__Ast.Make(F).impl_expr_kind ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_impl_ident : 
    unit ->
    Hax_engine__Ast.Make(F).impl_ident ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_impl_item : 
    unit ->
    Hax_engine__Ast.Make(F).impl_item ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_impl_item' : 
    unit ->
    Hax_engine__Ast.Make(F).impl_item' ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_int_kind : 
    unit ->
    Ast.int_kind ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_item : 
    unit ->
    Hax_engine__Ast.Make(F).item ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_item' : 
    unit ->
    Hax_engine__Ast.Make(F).item' ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_item_quote_origin : 
    unit ->
    Ast.item_quote_origin ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_lhs : 
    unit ->
    Hax_engine__Ast.Make(F).lhs ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_list : 
    'a. (unit ->
          'a ->
          (Local_ident.t, Local_ident.comparator_witness)
            Hax_engine.Prelude.Set.t) ->
    unit ->
    'a Base.list ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_literal : 
    unit ->
    Ast.literal ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_local_ident : 
    unit ->
    Ast.local_ident ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_loop_kind : 
    unit ->
    Hax_engine__Ast.Make(F).loop_kind ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_loop_state : 
    unit ->
    Hax_engine__Ast.Make(F).loop_state ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_modul : 
    unit ->
    Hax_engine__Ast.Make(F).item Prelude.list ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_mutability : 
    'mut_witness. (unit ->
                    'mut_witness ->
                    (Local_ident.t, Local_ident.comparator_witness)
                      Hax_engine.Prelude.Set.t) ->
    unit ->
    'mut_witness Ast.mutability ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_option : 
    'a. (unit ->
          'a ->
          (Local_ident.t, Local_ident.comparator_witness)
            Hax_engine.Prelude.Set.t) ->
    unit ->
    'a Base.option ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_param : 
    unit ->
    Hax_engine__Ast.Make(F).param ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_pat : 
    unit ->
    Hax_engine__Ast.Make(F).pat ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_pat' : 
    unit ->
    Hax_engine__Ast.Make(F).pat' ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_prim___tuple_2 : 
    't0 't1. (unit ->
               't0 ->
               (Local_ident.t, Local_ident.comparator_witness)
                 Hax_engine.Prelude.Set.t) ->
    (unit ->
      't1 ->
      (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t) ->
    unit ->
    ('t0 * 't1) ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_prim___tuple_3 : 
    't0 't1 't2. (unit ->
                   't0 ->
                   (Local_ident.t, Local_ident.comparator_witness)
                     Hax_engine.Prelude.Set.t) ->
    (unit ->
      't1 ->
      (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t) ->
    (unit ->
      't2 ->
      (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t) ->
    unit ->
    ('t0 * 't1 * 't2) ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_prim___tuple_4 : 
    't0 't1 't2 't3. (unit ->
                       't0 ->
                       (Local_ident.t, Local_ident.comparator_witness)
                         Hax_engine.Prelude.Set.t) ->
    (unit ->
      't1 ->
      (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t) ->
    (unit ->
      't2 ->
      (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t) ->
    (unit ->
      't3 ->
      (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t) ->
    unit ->
    ('t0 * 't1 * 't2 * 't3) ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_projection_predicate : 
    unit ->
    Hax_engine__Ast.Make(F).projection_predicate ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_quote : 
    unit ->
    Hax_engine__Ast.Make(F).quote ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_quote_content : 
    unit ->
    Hax_engine__Ast.Make(F).quote_content ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_safety_kind : 
    unit ->
    Hax_engine__Ast.Make(F).safety_kind ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_span : 
    unit ->
    Ast.span ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_string : 
    unit ->
    Base.string ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_supported_monads : 
    unit ->
    Hax_engine__Ast.Make(F).supported_monads ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_todo : 
    unit ->
    Ast.todo ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_trait_goal : 
    unit ->
    Hax_engine__Ast.Make(F).trait_goal ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_trait_item : 
    unit ->
    Hax_engine__Ast.Make(F).trait_item ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_trait_item' : 
    unit ->
    Hax_engine__Ast.Make(F).trait_item' ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_ty : 
    unit ->
    Hax_engine__Ast.Make(F).ty ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_variant : 
    unit ->
    Hax_engine__Ast.Make(F).variant ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t >

include sig ... end

val collect_ambiguous_local_idents : 'b Visitors.reduce as 'a

Rust macros are hygienic: even if a macro introduces a name that already exists in scope, the compiler will not shadow it. Instead, it will track and differentiate the two, even if those have the same name. `collect_ambiguous_local_idents` is a visitor that collects such "fake" shadowings.

val disambiguate_local_idents : AST.item -> AST.item

Rust macros are hygienic: even if a macro introduces a name that already exists in scope, the compiler will not shadow it. Instead, it will track and differentiate the two, even if those have the same name. `disambiguate_local_idents item` renames every instance of such a "fake" shadowing in `item`. See PR #368 for an example.

val collect_global_idents : 
  < visit_F__arbitrary_lhs : 
    Prelude.unit ->
    F.arbitrary_lhs ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__as_pattern : 
    Prelude.unit ->
    F.as_pattern ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__block : 
    Prelude.unit ->
    F.block ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__break : 
    Prelude.unit ->
    F.break ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__construct_base : 
    Prelude.unit ->
    F.construct_base ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__continue : 
    Prelude.unit ->
    F.continue ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__dyn : 
    Prelude.unit ->
    F.dyn ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__early_exit : 
    Prelude.unit ->
    F.early_exit ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__fold_like_loop : 
    Prelude.unit ->
    F.fold_like_loop ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__for_index_loop : 
    Prelude.unit ->
    F.for_index_loop ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__for_loop : 
    Prelude.unit ->
    F.for_loop ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__lifetime : 
    Prelude.unit ->
    F.lifetime ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__loop : 
    Prelude.unit ->
    F.loop ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__macro : 
    Prelude.unit ->
    F.macro ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__match_guard : 
    Prelude.unit ->
    F.match_guard ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__monadic_action : 
    Prelude.unit ->
    F.monadic_action ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__monadic_binding : 
    Prelude.unit ->
    F.monadic_binding ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__mutable_pointer : 
    Prelude.unit ->
    F.mutable_pointer ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__mutable_reference : 
    Prelude.unit ->
    F.mutable_reference ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__mutable_variable : 
    Prelude.unit ->
    F.mutable_variable ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__nontrivial_lhs : 
    Prelude.unit ->
    F.nontrivial_lhs ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__question_mark : 
    Prelude.unit ->
    F.question_mark ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__quote : 
    Prelude.unit ->
    F.quote ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__raw_pointer : 
    Prelude.unit ->
    F.raw_pointer ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__reference : 
    Prelude.unit ->
    F.reference ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__slice : 
    Prelude.unit ->
    F.slice ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__state_passing_loop : 
    Prelude.unit ->
    F.state_passing_loop ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__trait_item_default : 
    Prelude.unit ->
    F.trait_item_default ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__unsafe : 
    Prelude.unit ->
    F.unsafe ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__while_loop : 
    Prelude.unit ->
    F.while_loop ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_Local_ident__t : 
    Prelude.unit ->
    Local_ident.t ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_arm : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).arm ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_arm' : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).arm' ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_attr : 
    Prelude.unit ->
    Ast.attr ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_attrs : 
    Prelude.unit ->
    Ast.attrs ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_binding_mode : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).binding_mode ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_bool : 
    Prelude.unit ->
    Base.bool ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_borrow_kind : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).borrow_kind ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_cf_kind : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).cf_kind ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_char : 
    Prelude.unit ->
    Base.char ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_concrete_ident : 
    Prelude.unit ->
    Ast.concrete_ident ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_dyn_trait_goal : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).dyn_trait_goal ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_expr : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).expr ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_expr' : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).expr' ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_field_pat : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).field_pat ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_float_kind : 
    Prelude.unit ->
    Ast.float_kind ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_generic_constraint : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).generic_constraint ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_generic_param : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).generic_param ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_generic_param_kind : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).generic_param_kind ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_generic_value : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).generic_value ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_generics : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).generics ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_global_ident : 
    Prelude.unit ->
    Ast.global_ident ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_guard : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).guard ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_guard' : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).guard' ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_impl_expr : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).impl_expr ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_impl_expr_kind : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).impl_expr_kind ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_impl_ident : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).impl_ident ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_impl_item : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).impl_item ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_impl_item' : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).impl_item' ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_int_kind : 
    Prelude.unit ->
    Ast.int_kind ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_item : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).item ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_item' : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).item' ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_item_quote_origin : 
    Prelude.unit ->
    Ast.item_quote_origin ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_lhs : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).lhs ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_list : 
    'a. (Prelude.unit ->
          'a ->
          (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
            Hax_engine.Prelude.Set.t) ->
    Prelude.unit ->
    'a Base.list ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_literal : 
    Prelude.unit ->
    Ast.literal ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_local_ident : 
    Prelude.unit ->
    Ast.local_ident ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_loop_kind : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).loop_kind ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_loop_state : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).loop_state ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_modul : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).item Prelude.list ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_mutability : 
    'mut_witness. (Prelude.unit ->
                    'mut_witness ->
                    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
                      Hax_engine.Prelude.Set.t) ->
    Prelude.unit ->
    'mut_witness Ast.mutability ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_option : 
    'a. (Prelude.unit ->
          'a ->
          (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
            Hax_engine.Prelude.Set.t) ->
    Prelude.unit ->
    'a Base.option ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_param : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).param ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_pat : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).pat ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_pat' : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).pat' ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_prim___tuple_2 : 
    't0 't1. (Prelude.unit ->
               't0 ->
               (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
                 Hax_engine.Prelude.Set.t) ->
    (Prelude.unit ->
      't1 ->
      (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
        Hax_engine.Prelude.Set.t) ->
    Prelude.unit ->
    ('t0 * 't1) ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_prim___tuple_3 : 
    't0 't1 't2. (Prelude.unit ->
                   't0 ->
                   (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
                     Hax_engine.Prelude.Set.t) ->
    (Prelude.unit ->
      't1 ->
      (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
        Hax_engine.Prelude.Set.t) ->
    (Prelude.unit ->
      't2 ->
      (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
        Hax_engine.Prelude.Set.t) ->
    Prelude.unit ->
    ('t0 * 't1 * 't2) ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_prim___tuple_4 : 
    't0 't1 't2 't3. (Prelude.unit ->
                       't0 ->
                       (Ast.Global_ident.t,
                         Ast.Global_ident.comparator_witness)
                         Hax_engine.Prelude.Set.t) ->
    (Prelude.unit ->
      't1 ->
      (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
        Hax_engine.Prelude.Set.t) ->
    (Prelude.unit ->
      't2 ->
      (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
        Hax_engine.Prelude.Set.t) ->
    (Prelude.unit ->
      't3 ->
      (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
        Hax_engine.Prelude.Set.t) ->
    Prelude.unit ->
    ('t0 * 't1 * 't2 * 't3) ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_projection_predicate : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).projection_predicate ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_quote : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).quote ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_quote_content : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).quote_content ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_safety_kind : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).safety_kind ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_span : 
    Prelude.unit ->
    Ast.span ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_string : 
    Prelude.unit ->
    Base.string ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_supported_monads : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).supported_monads ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_todo : 
    Prelude.unit ->
    Ast.todo ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_trait_goal : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).trait_goal ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_trait_item : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).trait_item ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_trait_item' : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).trait_item' ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_ty : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).ty ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_variant : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).variant ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t >

val collect_concrete_idents : 
  < visit_F__arbitrary_lhs : 
    Prelude.unit ->
    F.arbitrary_lhs ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__as_pattern : 
    Prelude.unit ->
    F.as_pattern ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__block : 
    Prelude.unit ->
    F.block ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__break : 
    Prelude.unit ->
    F.break ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__construct_base : 
    Prelude.unit ->
    F.construct_base ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__continue : 
    Prelude.unit ->
    F.continue ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__dyn : 
    Prelude.unit ->
    F.dyn ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__early_exit : 
    Prelude.unit ->
    F.early_exit ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__fold_like_loop : 
    Prelude.unit ->
    F.fold_like_loop ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__for_index_loop : 
    Prelude.unit ->
    F.for_index_loop ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__for_loop : 
    Prelude.unit ->
    F.for_loop ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__lifetime : 
    Prelude.unit ->
    F.lifetime ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__loop : 
    Prelude.unit ->
    F.loop ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__macro : 
    Prelude.unit ->
    F.macro ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__match_guard : 
    Prelude.unit ->
    F.match_guard ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__monadic_action : 
    Prelude.unit ->
    F.monadic_action ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__monadic_binding : 
    Prelude.unit ->
    F.monadic_binding ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__mutable_pointer : 
    Prelude.unit ->
    F.mutable_pointer ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__mutable_reference : 
    Prelude.unit ->
    F.mutable_reference ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__mutable_variable : 
    Prelude.unit ->
    F.mutable_variable ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__nontrivial_lhs : 
    Prelude.unit ->
    F.nontrivial_lhs ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__question_mark : 
    Prelude.unit ->
    F.question_mark ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__quote : 
    Prelude.unit ->
    F.quote ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__raw_pointer : 
    Prelude.unit ->
    F.raw_pointer ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__reference : 
    Prelude.unit ->
    F.reference ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__slice : 
    Prelude.unit ->
    F.slice ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__state_passing_loop : 
    Prelude.unit ->
    F.state_passing_loop ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__trait_item_default : 
    Prelude.unit ->
    F.trait_item_default ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__unsafe : 
    Prelude.unit ->
    F.unsafe ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__while_loop : 
    Prelude.unit ->
    F.while_loop ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_Local_ident__t : 
    Prelude.unit ->
    Local_ident.t ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_arm : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).arm ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_arm' : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).arm' ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_attr : 
    Prelude.unit ->
    Ast.attr ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_attrs : 
    Prelude.unit ->
    Ast.attrs ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_binding_mode : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).binding_mode ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_bool : 
    Prelude.unit ->
    Base.bool ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_borrow_kind : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).borrow_kind ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_cf_kind : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).cf_kind ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_char : 
    Prelude.unit ->
    Base.char ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_concrete_ident : 
    Prelude.unit ->
    Ast.concrete_ident ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_dyn_trait_goal : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).dyn_trait_goal ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_expr : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).expr ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_expr' : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).expr' ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_field_pat : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).field_pat ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_float_kind : 
    Prelude.unit ->
    Ast.float_kind ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_generic_constraint : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).generic_constraint ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_generic_param : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).generic_param ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_generic_param_kind : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).generic_param_kind ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_generic_value : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).generic_value ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_generics : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).generics ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_global_ident : 
    Prelude.unit ->
    Ast.global_ident ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_guard : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).guard ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_guard' : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).guard' ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_impl_expr : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).impl_expr ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_impl_expr_kind : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).impl_expr_kind ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_impl_ident : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).impl_ident ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_impl_item : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).impl_item ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_impl_item' : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).impl_item' ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_int_kind : 
    Prelude.unit ->
    Ast.int_kind ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_item : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).item ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_item' : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).item' ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_item_quote_origin : 
    Prelude.unit ->
    Ast.item_quote_origin ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_lhs : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).lhs ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_list : 
    'a. (Prelude.unit ->
          'a ->
          (Concrete_ident.t, Concrete_ident.comparator_witness)
            Hax_engine.Prelude.Set.t) ->
    Prelude.unit ->
    'a Base.list ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_literal : 
    Prelude.unit ->
    Ast.literal ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_local_ident : 
    Prelude.unit ->
    Ast.local_ident ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_loop_kind : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).loop_kind ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_loop_state : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).loop_state ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_modul : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).item Prelude.list ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_mutability : 
    'mut_witness. (Prelude.unit ->
                    'mut_witness ->
                    (Concrete_ident.t, Concrete_ident.comparator_witness)
                      Hax_engine.Prelude.Set.t) ->
    Prelude.unit ->
    'mut_witness Ast.mutability ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_option : 
    'a. (Prelude.unit ->
          'a ->
          (Concrete_ident.t, Concrete_ident.comparator_witness)
            Hax_engine.Prelude.Set.t) ->
    Prelude.unit ->
    'a Base.option ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_param : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).param ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_pat : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).pat ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_pat' : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).pat' ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_prim___tuple_2 : 
    't0 't1. (Prelude.unit ->
               't0 ->
               (Concrete_ident.t, Concrete_ident.comparator_witness)
                 Hax_engine.Prelude.Set.t) ->
    (Prelude.unit ->
      't1 ->
      (Concrete_ident.t, Concrete_ident.comparator_witness)
        Hax_engine.Prelude.Set.t) ->
    Prelude.unit ->
    ('t0 * 't1) ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_prim___tuple_3 : 
    't0 't1 't2. (Prelude.unit ->
                   't0 ->
                   (Concrete_ident.t, Concrete_ident.comparator_witness)
                     Hax_engine.Prelude.Set.t) ->
    (Prelude.unit ->
      't1 ->
      (Concrete_ident.t, Concrete_ident.comparator_witness)
        Hax_engine.Prelude.Set.t) ->
    (Prelude.unit ->
      't2 ->
      (Concrete_ident.t, Concrete_ident.comparator_witness)
        Hax_engine.Prelude.Set.t) ->
    Prelude.unit ->
    ('t0 * 't1 * 't2) ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_prim___tuple_4 : 
    't0 't1 't2 't3. (Prelude.unit ->
                       't0 ->
                       (Concrete_ident.t, Concrete_ident.comparator_witness)
                         Hax_engine.Prelude.Set.t) ->
    (Prelude.unit ->
      't1 ->
      (Concrete_ident.t, Concrete_ident.comparator_witness)
        Hax_engine.Prelude.Set.t) ->
    (Prelude.unit ->
      't2 ->
      (Concrete_ident.t, Concrete_ident.comparator_witness)
        Hax_engine.Prelude.Set.t) ->
    (Prelude.unit ->
      't3 ->
      (Concrete_ident.t, Concrete_ident.comparator_witness)
        Hax_engine.Prelude.Set.t) ->
    Prelude.unit ->
    ('t0 * 't1 * 't2 * 't3) ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_projection_predicate : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).projection_predicate ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_quote : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).quote ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_quote_content : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).quote_content ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_safety_kind : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).safety_kind ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_span : 
    Prelude.unit ->
    Ast.span ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_string : 
    Prelude.unit ->
    Base.string ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_supported_monads : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).supported_monads ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_todo : 
    Prelude.unit ->
    Ast.todo ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_trait_goal : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).trait_goal ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_trait_item : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).trait_item ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_trait_item' : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).trait_item' ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_ty : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).ty ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_variant : 
    Prelude.unit ->
    Hax_engine__Ast.Make(F).variant ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t >

val variables_of_pat : AST.pat -> Sets.Local_ident.t

val variables_of_param : AST.param -> Local_ident.t Prelude.list

val variables_of_pats : AST.pat Prelude.list -> Sets.Local_ident.t

val without_vars : 
  Sets.TypedLocalIdent.t ->
  Sets.Local_ident.t ->
  (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
    Hax_engine.Prelude.Set.t

val without_pats_vars : 
  Sets.TypedLocalIdent.t ->
  AST.pat Prelude.list ->
  Sets.TypedLocalIdent.t

val without_pat_vars : 
  Sets.TypedLocalIdent.t ->
  AST.pat ->
  Sets.TypedLocalIdent.t

val free_assigned_variables : 
  (F.arbitrary_lhs -> AST.expr -> Sets.TypedLocalIdent.t) ->
  < visit_F__arbitrary_lhs : 
    unit ->
    F.arbitrary_lhs ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__as_pattern : 
    unit ->
    F.as_pattern ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__block : 
    unit ->
    F.block ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__break : 
    unit ->
    F.break ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__construct_base : 
    unit ->
    F.construct_base ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__continue : 
    unit ->
    F.continue ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__dyn : 
    unit ->
    F.dyn ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__early_exit : 
    unit ->
    F.early_exit ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__fold_like_loop : 
    unit ->
    F.fold_like_loop ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__for_index_loop : 
    unit ->
    F.for_index_loop ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__for_loop : 
    unit ->
    F.for_loop ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__lifetime : 
    unit ->
    F.lifetime ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__loop : 
    unit ->
    F.loop ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__macro : 
    unit ->
    F.macro ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__match_guard : 
    unit ->
    F.match_guard ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__monadic_action : 
    unit ->
    F.monadic_action ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__monadic_binding : 
    unit ->
    F.monadic_binding ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__mutable_pointer : 
    unit ->
    F.mutable_pointer ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__mutable_reference : 
    unit ->
    F.mutable_reference ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__mutable_variable : 
    unit ->
    F.mutable_variable ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__nontrivial_lhs : 
    unit ->
    F.nontrivial_lhs ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__question_mark : 
    unit ->
    F.question_mark ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__quote : 
    unit ->
    F.quote ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__raw_pointer : 
    unit ->
    F.raw_pointer ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__reference : 
    unit ->
    F.reference ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__slice : 
    unit ->
    F.slice ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__state_passing_loop : 
    unit ->
    F.state_passing_loop ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__trait_item_default : 
    unit ->
    F.trait_item_default ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__unsafe : 
    unit ->
    F.unsafe ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__while_loop : 
    unit ->
    F.while_loop ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_Local_ident__t : 
    unit ->
    Local_ident.t ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_arm : 
    unit ->
    Hax_engine__Ast.Make(F).arm ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_arm' : 
    unit ->
    Hax_engine__Ast.Make(F).arm' ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_attr : 
    unit ->
    Ast.attr ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_attrs : 
    unit ->
    Ast.attrs ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_binding_mode : 
    unit ->
    Hax_engine__Ast.Make(F).binding_mode ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_bool : 
    unit ->
    Base.bool ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_borrow_kind : 
    unit ->
    Hax_engine__Ast.Make(F).borrow_kind ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_cf_kind : 
    unit ->
    Hax_engine__Ast.Make(F).cf_kind ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_char : 
    unit ->
    Base.char ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_concrete_ident : 
    unit ->
    Ast.concrete_ident ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_dyn_trait_goal : 
    unit ->
    Hax_engine__Ast.Make(F).dyn_trait_goal ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_expr : 
    unit ->
    Hax_engine__Ast.Make(F).expr ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_expr' : 
    unit ->
    Hax_engine__Ast.Make(F).expr' ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_field_pat : 
    unit ->
    Hax_engine__Ast.Make(F).field_pat ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_float_kind : 
    unit ->
    Ast.float_kind ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_generic_constraint : 
    unit ->
    Hax_engine__Ast.Make(F).generic_constraint ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_generic_param : 
    unit ->
    Hax_engine__Ast.Make(F).generic_param ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_generic_param_kind : 
    unit ->
    Hax_engine__Ast.Make(F).generic_param_kind ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_generic_value : 
    unit ->
    Hax_engine__Ast.Make(F).generic_value ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_generics : 
    unit ->
    Hax_engine__Ast.Make(F).generics ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_global_ident : 
    unit ->
    Ast.global_ident ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_guard : 
    unit ->
    Hax_engine__Ast.Make(F).guard ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_guard' : 
    unit ->
    Hax_engine__Ast.Make(F).guard' ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_impl_expr : 
    unit ->
    Hax_engine__Ast.Make(F).impl_expr ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_impl_expr_kind : 
    unit ->
    Hax_engine__Ast.Make(F).impl_expr_kind ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_impl_ident : 
    unit ->
    Hax_engine__Ast.Make(F).impl_ident ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_impl_item : 
    unit ->
    Hax_engine__Ast.Make(F).impl_item ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_impl_item' : 
    unit ->
    Hax_engine__Ast.Make(F).impl_item' ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_int_kind : 
    unit ->
    Ast.int_kind ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_item : 
    unit ->
    Hax_engine__Ast.Make(F).item ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_item' : 
    unit ->
    Hax_engine__Ast.Make(F).item' ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_item_quote_origin : 
    unit ->
    Ast.item_quote_origin ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_lhs : 
    unit ->
    Hax_engine__Ast.Make(F).lhs ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_list : 
    'a. (unit ->
          'a ->
          (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
            Hax_engine.Prelude.Set.t) ->
    unit ->
    'a Base.list ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_literal : 
    unit ->
    Ast.literal ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_local_ident : 
    unit ->
    Ast.local_ident ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_loop_kind : 
    unit ->
    Hax_engine__Ast.Make(F).loop_kind ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_loop_state : 
    unit ->
    Hax_engine__Ast.Make(F).loop_state ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_modul : 
    unit ->
    Hax_engine__Ast.Make(F).item Prelude.list ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_mutability : 
    'mut_witness. (unit ->
                    'mut_witness ->
                    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
                      Hax_engine.Prelude.Set.t) ->
    unit ->
    'mut_witness Ast.mutability ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_option : 
    'a. (unit ->
          'a ->
          (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
            Hax_engine.Prelude.Set.t) ->
    unit ->
    'a Base.option ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_param : 
    unit ->
    Hax_engine__Ast.Make(F).param ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_pat : 
    unit ->
    Hax_engine__Ast.Make(F).pat ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_pat' : 
    unit ->
    Hax_engine__Ast.Make(F).pat' ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_prim___tuple_2 : 
    't0 't1. (unit ->
               't0 ->
               (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
                 Hax_engine.Prelude.Set.t) ->
    (unit ->
      't1 ->
      (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
        Hax_engine.Prelude.Set.t) ->
    unit ->
    ('t0 * 't1) ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_prim___tuple_3 : 
    't0 't1 't2. (unit ->
                   't0 ->
                   (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
                     Hax_engine.Prelude.Set.t) ->
    (unit ->
      't1 ->
      (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
        Hax_engine.Prelude.Set.t) ->
    (unit ->
      't2 ->
      (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
        Hax_engine.Prelude.Set.t) ->
    unit ->
    ('t0 * 't1 * 't2) ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_prim___tuple_4 : 
    't0 't1 't2 't3. (unit ->
                       't0 ->
                       (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
                         Hax_engine.Prelude.Set.t) ->
    (unit ->
      't1 ->
      (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
        Hax_engine.Prelude.Set.t) ->
    (unit ->
      't2 ->
      (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
        Hax_engine.Prelude.Set.t) ->
    (unit ->
      't3 ->
      (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
        Hax_engine.Prelude.Set.t) ->
    unit ->
    ('t0 * 't1 * 't2 * 't3) ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_projection_predicate : 
    unit ->
    Hax_engine__Ast.Make(F).projection_predicate ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_quote : 
    unit ->
    Hax_engine__Ast.Make(F).quote ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_quote_content : 
    unit ->
    Hax_engine__Ast.Make(F).quote_content ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_safety_kind : 
    unit ->
    Hax_engine__Ast.Make(F).safety_kind ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_span : 
    unit ->
    Ast.span ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_string : 
    unit ->
    Base.string ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_supported_monads : 
    unit ->
    Hax_engine__Ast.Make(F).supported_monads ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_todo : 
    unit ->
    Ast.todo ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_trait_goal : 
    unit ->
    Hax_engine__Ast.Make(F).trait_goal ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_trait_item : 
    unit ->
    Hax_engine__Ast.Make(F).trait_item ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_trait_item' : 
    unit ->
    Hax_engine__Ast.Make(F).trait_item' ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_ty : 
    unit ->
    Hax_engine__Ast.Make(F).ty ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_variant : 
    unit ->
    Hax_engine__Ast.Make(F).variant ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t >

class 's expr_list_monoid : object ... end

val collect_break_payloads : 
  < visit_F__arbitrary_lhs : 
    unit ->
    F.arbitrary_lhs ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__as_pattern : 
    unit ->
    F.as_pattern ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__block : unit -> F.block -> AST.expr Hax_engine.Prelude.List.t
  ; visit_F__break : unit -> F.break -> AST.expr Hax_engine.Prelude.List.t
  ; visit_F__construct_base : 
    unit ->
    F.construct_base ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__continue : 
    unit ->
    F.continue ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__dyn : unit -> F.dyn -> AST.expr Hax_engine.Prelude.List.t
  ; visit_F__early_exit : 
    unit ->
    F.early_exit ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__fold_like_loop : 
    unit ->
    F.fold_like_loop ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__for_index_loop : 
    unit ->
    F.for_index_loop ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__for_loop : 
    unit ->
    F.for_loop ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__lifetime : 
    unit ->
    F.lifetime ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__loop : unit -> F.loop -> AST.expr Hax_engine.Prelude.List.t
  ; visit_F__macro : unit -> F.macro -> AST.expr Hax_engine.Prelude.List.t
  ; visit_F__match_guard : 
    unit ->
    F.match_guard ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__monadic_action : 
    unit ->
    F.monadic_action ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__monadic_binding : 
    unit ->
    F.monadic_binding ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__mutable_pointer : 
    unit ->
    F.mutable_pointer ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__mutable_reference : 
    unit ->
    F.mutable_reference ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__mutable_variable : 
    unit ->
    F.mutable_variable ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__nontrivial_lhs : 
    unit ->
    F.nontrivial_lhs ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__question_mark : 
    unit ->
    F.question_mark ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__quote : unit -> F.quote -> AST.expr Hax_engine.Prelude.List.t
  ; visit_F__raw_pointer : 
    unit ->
    F.raw_pointer ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__reference : 
    unit ->
    F.reference ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__slice : unit -> F.slice -> AST.expr Hax_engine.Prelude.List.t
  ; visit_F__state_passing_loop : 
    unit ->
    F.state_passing_loop ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__trait_item_default : 
    unit ->
    F.trait_item_default ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__unsafe : unit -> F.unsafe -> AST.expr Hax_engine.Prelude.List.t
  ; visit_F__while_loop : 
    unit ->
    F.while_loop ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_Local_ident__t : 
    unit ->
    Local_ident.t ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_arm : 
    unit ->
    Hax_engine__Ast.Make(F).arm ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_arm' : 
    unit ->
    Hax_engine__Ast.Make(F).arm' ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_attr : unit -> Ast.attr -> AST.expr Hax_engine.Prelude.List.t
  ; visit_attrs : unit -> Ast.attrs -> AST.expr Hax_engine.Prelude.List.t
  ; visit_binding_mode : 
    unit ->
    Hax_engine__Ast.Make(F).binding_mode ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_bool : unit -> Base.bool -> AST.expr Hax_engine.Prelude.List.t
  ; visit_borrow_kind : 
    unit ->
    Hax_engine__Ast.Make(F).borrow_kind ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_cf_kind : 
    unit ->
    Hax_engine__Ast.Make(F).cf_kind ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_char : unit -> Base.char -> AST.expr Hax_engine.Prelude.List.t
  ; visit_concrete_ident : 
    unit ->
    Ast.concrete_ident ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_dyn_trait_goal : 
    unit ->
    Hax_engine__Ast.Make(F).dyn_trait_goal ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_expr : 
    unit ->
    Hax_engine__Ast.Make(F).expr ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_expr' : 
    unit ->
    Hax_engine__Ast.Make(F).expr' ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_field_pat : 
    unit ->
    Hax_engine__Ast.Make(F).field_pat ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_float_kind : 
    unit ->
    Ast.float_kind ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_generic_constraint : 
    unit ->
    Hax_engine__Ast.Make(F).generic_constraint ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_generic_param : 
    unit ->
    Hax_engine__Ast.Make(F).generic_param ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_generic_param_kind : 
    unit ->
    Hax_engine__Ast.Make(F).generic_param_kind ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_generic_value : 
    unit ->
    Hax_engine__Ast.Make(F).generic_value ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_generics : 
    unit ->
    Hax_engine__Ast.Make(F).generics ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_global_ident : 
    unit ->
    Ast.global_ident ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_guard : 
    unit ->
    Hax_engine__Ast.Make(F).guard ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_guard' : 
    unit ->
    Hax_engine__Ast.Make(F).guard' ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_impl_expr : 
    unit ->
    Hax_engine__Ast.Make(F).impl_expr ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_impl_expr_kind : 
    unit ->
    Hax_engine__Ast.Make(F).impl_expr_kind ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_impl_ident : 
    unit ->
    Hax_engine__Ast.Make(F).impl_ident ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_impl_item : 
    unit ->
    Hax_engine__Ast.Make(F).impl_item ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_impl_item' : 
    unit ->
    Hax_engine__Ast.Make(F).impl_item' ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_int_kind : unit -> Ast.int_kind -> AST.expr Hax_engine.Prelude.List.t
  ; visit_item : 
    unit ->
    Hax_engine__Ast.Make(F).item ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_item' : 
    unit ->
    Hax_engine__Ast.Make(F).item' ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_item_quote_origin : 
    unit ->
    Ast.item_quote_origin ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_lhs : 
    unit ->
    Hax_engine__Ast.Make(F).lhs ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_list : 
    'a. (unit -> 'a -> AST.expr Hax_engine.Prelude.List.t) ->
    unit ->
    'a Base.list ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_literal : unit -> Ast.literal -> AST.expr Hax_engine.Prelude.List.t
  ; visit_local_ident : 
    unit ->
    Ast.local_ident ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_loop_kind : 
    unit ->
    Hax_engine__Ast.Make(F).loop_kind ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_loop_state : 
    unit ->
    Hax_engine__Ast.Make(F).loop_state ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_modul : 
    unit ->
    Hax_engine__Ast.Make(F).item Prelude.list ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_mutability : 
    'mut_witness. (unit -> 'mut_witness -> AST.expr Hax_engine.Prelude.List.t) ->
    unit ->
    'mut_witness Ast.mutability ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_option : 
    'a. (unit -> 'a -> AST.expr Hax_engine.Prelude.List.t) ->
    unit ->
    'a Base.option ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_param : 
    unit ->
    Hax_engine__Ast.Make(F).param ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_pat : 
    unit ->
    Hax_engine__Ast.Make(F).pat ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_pat' : 
    unit ->
    Hax_engine__Ast.Make(F).pat' ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_prim___tuple_2 : 
    't0 't1. (unit -> 't0 -> AST.expr Hax_engine.Prelude.List.t) ->
    (unit -> 't1 -> AST.expr Hax_engine.Prelude.List.t) ->
    unit ->
    ('t0 * 't1) ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_prim___tuple_3 : 
    't0 't1 't2. (unit -> 't0 -> AST.expr Hax_engine.Prelude.List.t) ->
    (unit -> 't1 -> AST.expr Hax_engine.Prelude.List.t) ->
    (unit -> 't2 -> AST.expr Hax_engine.Prelude.List.t) ->
    unit ->
    ('t0 * 't1 * 't2) ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_prim___tuple_4 : 
    't0 't1 't2 't3. (unit -> 't0 -> AST.expr Hax_engine.Prelude.List.t) ->
    (unit -> 't1 -> AST.expr Hax_engine.Prelude.List.t) ->
    (unit -> 't2 -> AST.expr Hax_engine.Prelude.List.t) ->
    (unit -> 't3 -> AST.expr Hax_engine.Prelude.List.t) ->
    unit ->
    ('t0 * 't1 * 't2 * 't3) ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_projection_predicate : 
    unit ->
    Hax_engine__Ast.Make(F).projection_predicate ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_quote : 
    unit ->
    Hax_engine__Ast.Make(F).quote ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_quote_content : 
    unit ->
    Hax_engine__Ast.Make(F).quote_content ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_safety_kind : 
    unit ->
    Hax_engine__Ast.Make(F).safety_kind ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_span : unit -> Ast.span -> AST.expr Hax_engine.Prelude.List.t
  ; visit_string : unit -> Base.string -> AST.expr Hax_engine.Prelude.List.t
  ; visit_supported_monads : 
    unit ->
    Hax_engine__Ast.Make(F).supported_monads ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_todo : unit -> Ast.todo -> AST.expr Hax_engine.Prelude.List.t
  ; visit_trait_goal : 
    unit ->
    Hax_engine__Ast.Make(F).trait_goal ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_trait_item : 
    unit ->
    Hax_engine__Ast.Make(F).trait_item ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_trait_item' : 
    unit ->
    Hax_engine__Ast.Make(F).trait_item' ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_ty : 
    unit ->
    Hax_engine__Ast.Make(F).ty ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_variant : 
    unit ->
    Hax_engine__Ast.Make(F).variant ->
    AST.expr Hax_engine.Prelude.List.t >

val collect_attrs : 
  < visit_F__arbitrary_lhs : 
    unit ->
    F.arbitrary_lhs ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_F__as_pattern : 
    unit ->
    F.as_pattern ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_F__block : unit -> F.block -> Ast.attr Hax_engine.Prelude.List.t
  ; visit_F__break : unit -> F.break -> Ast.attr Hax_engine.Prelude.List.t
  ; visit_F__construct_base : 
    unit ->
    F.construct_base ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_F__continue : 
    unit ->
    F.continue ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_F__dyn : unit -> F.dyn -> Ast.attr Hax_engine.Prelude.List.t
  ; visit_F__early_exit : 
    unit ->
    F.early_exit ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_F__fold_like_loop : 
    unit ->
    F.fold_like_loop ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_F__for_index_loop : 
    unit ->
    F.for_index_loop ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_F__for_loop : 
    unit ->
    F.for_loop ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_F__lifetime : 
    unit ->
    F.lifetime ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_F__loop : unit -> F.loop -> Ast.attr Hax_engine.Prelude.List.t
  ; visit_F__macro : unit -> F.macro -> Ast.attr Hax_engine.Prelude.List.t
  ; visit_F__match_guard : 
    unit ->
    F.match_guard ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_F__monadic_action : 
    unit ->
    F.monadic_action ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_F__monadic_binding : 
    unit ->
    F.monadic_binding ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_F__mutable_pointer : 
    unit ->
    F.mutable_pointer ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_F__mutable_reference : 
    unit ->
    F.mutable_reference ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_F__mutable_variable : 
    unit ->
    F.mutable_variable ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_F__nontrivial_lhs : 
    unit ->
    F.nontrivial_lhs ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_F__question_mark : 
    unit ->
    F.question_mark ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_F__quote : unit -> F.quote -> Ast.attr Hax_engine.Prelude.List.t
  ; visit_F__raw_pointer : 
    unit ->
    F.raw_pointer ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_F__reference : 
    unit ->
    F.reference ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_F__slice : unit -> F.slice -> Ast.attr Hax_engine.Prelude.List.t
  ; visit_F__state_passing_loop : 
    unit ->
    F.state_passing_loop ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_F__trait_item_default : 
    unit ->
    F.trait_item_default ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_F__unsafe : unit -> F.unsafe -> Ast.attr Hax_engine.Prelude.List.t
  ; visit_F__while_loop : 
    unit ->
    F.while_loop ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_Local_ident__t : 
    unit ->
    Local_ident.t ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_arm : 
    unit ->
    Hax_engine__Ast.Make(F).arm ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_arm' : 
    unit ->
    Hax_engine__Ast.Make(F).arm' ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_attr : unit -> Ast.attr -> Ast.attr Hax_engine.Prelude.List.t
  ; visit_attrs : unit -> Ast.attrs -> Ast.attr Hax_engine.Prelude.List.t
  ; visit_binding_mode : 
    unit ->
    Hax_engine__Ast.Make(F).binding_mode ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_bool : unit -> Base.bool -> Ast.attr Hax_engine.Prelude.List.t
  ; visit_borrow_kind : 
    unit ->
    Hax_engine__Ast.Make(F).borrow_kind ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_cf_kind : 
    unit ->
    Hax_engine__Ast.Make(F).cf_kind ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_char : unit -> Base.char -> Ast.attr Hax_engine.Prelude.List.t
  ; visit_concrete_ident : 
    unit ->
    Ast.concrete_ident ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_dyn_trait_goal : 
    unit ->
    Hax_engine__Ast.Make(F).dyn_trait_goal ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_expr : 
    unit ->
    Hax_engine__Ast.Make(F).expr ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_expr' : 
    unit ->
    Hax_engine__Ast.Make(F).expr' ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_field_pat : 
    unit ->
    Hax_engine__Ast.Make(F).field_pat ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_float_kind : 
    unit ->
    Ast.float_kind ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_generic_constraint : 
    unit ->
    Hax_engine__Ast.Make(F).generic_constraint ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_generic_param : 
    unit ->
    Hax_engine__Ast.Make(F).generic_param ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_generic_param_kind : 
    unit ->
    Hax_engine__Ast.Make(F).generic_param_kind ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_generic_value : 
    unit ->
    Hax_engine__Ast.Make(F).generic_value ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_generics : 
    unit ->
    Hax_engine__Ast.Make(F).generics ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_global_ident : 
    unit ->
    Ast.global_ident ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_guard : 
    unit ->
    Hax_engine__Ast.Make(F).guard ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_guard' : 
    unit ->
    Hax_engine__Ast.Make(F).guard' ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_impl_expr : 
    unit ->
    Hax_engine__Ast.Make(F).impl_expr ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_impl_expr_kind : 
    unit ->
    Hax_engine__Ast.Make(F).impl_expr_kind ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_impl_ident : 
    unit ->
    Hax_engine__Ast.Make(F).impl_ident ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_impl_item : 
    unit ->
    Hax_engine__Ast.Make(F).impl_item ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_impl_item' : 
    unit ->
    Hax_engine__Ast.Make(F).impl_item' ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_int_kind : unit -> Ast.int_kind -> Ast.attr Hax_engine.Prelude.List.t
  ; visit_item : 
    unit ->
    Hax_engine__Ast.Make(F).item ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_item' : 
    unit ->
    Hax_engine__Ast.Make(F).item' ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_item_quote_origin : 
    unit ->
    Ast.item_quote_origin ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_lhs : 
    unit ->
    Hax_engine__Ast.Make(F).lhs ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_list : 
    'a. (unit -> 'a -> Ast.attr Hax_engine.Prelude.List.t) ->
    unit ->
    'a Base.list ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_literal : unit -> Ast.literal -> Ast.attr Hax_engine.Prelude.List.t
  ; visit_local_ident : 
    unit ->
    Ast.local_ident ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_loop_kind : 
    unit ->
    Hax_engine__Ast.Make(F).loop_kind ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_loop_state : 
    unit ->
    Hax_engine__Ast.Make(F).loop_state ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_modul : 
    unit ->
    Hax_engine__Ast.Make(F).item Prelude.list ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_mutability : 
    'mut_witness. (unit -> 'mut_witness -> Ast.attr Hax_engine.Prelude.List.t) ->
    unit ->
    'mut_witness Ast.mutability ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_option : 
    'a. (unit -> 'a -> Ast.attr Hax_engine.Prelude.List.t) ->
    unit ->
    'a Base.option ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_param : 
    unit ->
    Hax_engine__Ast.Make(F).param ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_pat : 
    unit ->
    Hax_engine__Ast.Make(F).pat ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_pat' : 
    unit ->
    Hax_engine__Ast.Make(F).pat' ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_prim___tuple_2 : 
    't0 't1. (unit -> 't0 -> Ast.attr Hax_engine.Prelude.List.t) ->
    (unit -> 't1 -> Ast.attr Hax_engine.Prelude.List.t) ->
    unit ->
    ('t0 * 't1) ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_prim___tuple_3 : 
    't0 't1 't2. (unit -> 't0 -> Ast.attr Hax_engine.Prelude.List.t) ->
    (unit -> 't1 -> Ast.attr Hax_engine.Prelude.List.t) ->
    (unit -> 't2 -> Ast.attr Hax_engine.Prelude.List.t) ->
    unit ->
    ('t0 * 't1 * 't2) ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_prim___tuple_4 : 
    't0 't1 't2 't3. (unit -> 't0 -> Ast.attr Hax_engine.Prelude.List.t) ->
    (unit -> 't1 -> Ast.attr Hax_engine.Prelude.List.t) ->
    (unit -> 't2 -> Ast.attr Hax_engine.Prelude.List.t) ->
    (unit -> 't3 -> Ast.attr Hax_engine.Prelude.List.t) ->
    unit ->
    ('t0 * 't1 * 't2 * 't3) ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_projection_predicate : 
    unit ->
    Hax_engine__Ast.Make(F).projection_predicate ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_quote : 
    unit ->
    Hax_engine__Ast.Make(F).quote ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_quote_content : 
    unit ->
    Hax_engine__Ast.Make(F).quote_content ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_safety_kind : 
    unit ->
    Hax_engine__Ast.Make(F).safety_kind ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_span : unit -> Ast.span -> Ast.attr Hax_engine.Prelude.List.t
  ; visit_string : unit -> Base.string -> Ast.attr Hax_engine.Prelude.List.t
  ; visit_supported_monads : 
    unit ->
    Hax_engine__Ast.Make(F).supported_monads ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_todo : unit -> Ast.todo -> Ast.attr Hax_engine.Prelude.List.t
  ; visit_trait_goal : 
    unit ->
    Hax_engine__Ast.Make(F).trait_goal ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_trait_item : 
    unit ->
    Hax_engine__Ast.Make(F).trait_item ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_trait_item' : 
    unit ->
    Hax_engine__Ast.Make(F).trait_item' ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_ty : 
    unit ->
    Hax_engine__Ast.Make(F).ty ->
    Ast.attr Hax_engine.Prelude.List.t
  ; visit_variant : 
    unit ->
    Hax_engine__Ast.Make(F).variant ->
    Ast.attr Hax_engine.Prelude.List.t >