Reducers (hax-engine.Hax_engine.Phase_reject.RawOrMutPointer.UA.Reducers)

val collect_local_idents : 
  < visit_F__arbitrary_lhs : 
    unit ->
    FA.arbitrary_lhs ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__as_pattern : 
    unit ->
    FA.as_pattern ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__block : 
    unit ->
    FA.block ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__break : 
    unit ->
    FA.break ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__construct_base : 
    unit ->
    FA.construct_base ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__continue : 
    unit ->
    FA.continue ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__dyn : 
    unit ->
    FA.dyn ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__early_exit : 
    unit ->
    FA.early_exit ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__for_index_loop : 
    unit ->
    FA.for_index_loop ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__for_loop : 
    unit ->
    FA.for_loop ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__lifetime : 
    unit ->
    FA.lifetime ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__loop : 
    unit ->
    FA.loop ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__macro : 
    unit ->
    FA.macro ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__match_guard : 
    unit ->
    FA.match_guard ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__monadic_action : 
    unit ->
    FA.monadic_action ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__monadic_binding : 
    unit ->
    FA.monadic_binding ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__mutable_pointer : 
    unit ->
    FA.mutable_pointer ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__mutable_reference : 
    unit ->
    FA.mutable_reference ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__mutable_variable : 
    unit ->
    FA.mutable_variable ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__nontrivial_lhs : 
    unit ->
    FA.nontrivial_lhs ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__question_mark : 
    unit ->
    FA.question_mark ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__raw_pointer : 
    unit ->
    FA.raw_pointer ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__reference : 
    unit ->
    FA.reference ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__slice : 
    unit ->
    FA.slice ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__state_passing_loop : 
    unit ->
    FA.state_passing_loop ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__trait_item_default : 
    unit ->
    FA.trait_item_default ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__unsafe : 
    unit ->
    FA.unsafe ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_F__while_loop : 
    unit ->
    FA.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(FA).arm ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_arm' : 
    unit ->
    Hax_engine__Ast.Make(FA).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(FA).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(FA).borrow_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(FA).dyn_trait_goal ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_expr : 
    unit ->
    Hax_engine__Ast.Make(FA).expr ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_expr' : 
    unit ->
    Hax_engine__Ast.Make(FA).expr' ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_field_pat : 
    unit ->
    Hax_engine__Ast.Make(FA).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(FA).generic_constraint ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_generic_param : 
    unit ->
    Hax_engine__Ast.Make(FA).generic_param ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_generic_param_kind : 
    unit ->
    Hax_engine__Ast.Make(FA).generic_param_kind ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_generic_value : 
    unit ->
    Hax_engine__Ast.Make(FA).generic_value ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_generics : 
    unit ->
    Hax_engine__Ast.Make(FA).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(FA).guard ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_guard' : 
    unit ->
    Hax_engine__Ast.Make(FA).guard' ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_impl_expr : 
    unit ->
    Hax_engine__Ast.Make(FA).impl_expr ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_impl_expr_kind : 
    unit ->
    Hax_engine__Ast.Make(FA).impl_expr_kind ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_impl_ident : 
    unit ->
    Hax_engine__Ast.Make(FA).impl_ident ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_impl_item : 
    unit ->
    Hax_engine__Ast.Make(FA).impl_item ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_impl_item' : 
    unit ->
    Hax_engine__Ast.Make(FA).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(FA).item ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_item' : 
    unit ->
    Hax_engine__Ast.Make(FA).item' ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_lhs : 
    unit ->
    Hax_engine__Ast.Make(FA).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(FA).loop_kind ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_loop_state : 
    unit ->
    Hax_engine__Ast.Make(FA).loop_state ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_modul : 
    unit ->
    Hax_engine__Ast.Make(FA).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(FA).param ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_pat : 
    unit ->
    Hax_engine__Ast.Make(FA).pat ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_pat' : 
    unit ->
    Hax_engine__Ast.Make(FA).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(FA).projection_predicate ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_quote : 
    unit ->
    Hax_engine__Ast.Make(FA).quote ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_safety_kind : 
    unit ->
    Hax_engine__Ast.Make(FA).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(FA).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(FA).trait_goal ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_trait_item : 
    unit ->
    Hax_engine__Ast.Make(FA).trait_item ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_trait_item' : 
    unit ->
    Hax_engine__Ast.Make(FA).trait_item' ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_ty : 
    unit ->
    Hax_engine__Ast.Make(FA).ty ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t
  ; visit_variant : 
    unit ->
    Hax_engine__Ast.Make(FA).variant ->
    (Local_ident.t, Local_ident.comparator_witness) Hax_engine.Prelude.Set.t >

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

val disambiguate_local_idents : AST.item -> AST.item

val collect_global_idents : 
  < visit_F__arbitrary_lhs : 
    Prelude.unit ->
    FA.arbitrary_lhs ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__as_pattern : 
    Prelude.unit ->
    FA.as_pattern ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__block : 
    Prelude.unit ->
    FA.block ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__break : 
    Prelude.unit ->
    FA.break ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__construct_base : 
    Prelude.unit ->
    FA.construct_base ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__continue : 
    Prelude.unit ->
    FA.continue ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__dyn : 
    Prelude.unit ->
    FA.dyn ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__early_exit : 
    Prelude.unit ->
    FA.early_exit ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__for_index_loop : 
    Prelude.unit ->
    FA.for_index_loop ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__for_loop : 
    Prelude.unit ->
    FA.for_loop ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__lifetime : 
    Prelude.unit ->
    FA.lifetime ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__loop : 
    Prelude.unit ->
    FA.loop ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__macro : 
    Prelude.unit ->
    FA.macro ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__match_guard : 
    Prelude.unit ->
    FA.match_guard ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__monadic_action : 
    Prelude.unit ->
    FA.monadic_action ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__monadic_binding : 
    Prelude.unit ->
    FA.monadic_binding ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__mutable_pointer : 
    Prelude.unit ->
    FA.mutable_pointer ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__mutable_reference : 
    Prelude.unit ->
    FA.mutable_reference ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__mutable_variable : 
    Prelude.unit ->
    FA.mutable_variable ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__nontrivial_lhs : 
    Prelude.unit ->
    FA.nontrivial_lhs ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__question_mark : 
    Prelude.unit ->
    FA.question_mark ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__raw_pointer : 
    Prelude.unit ->
    FA.raw_pointer ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__reference : 
    Prelude.unit ->
    FA.reference ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__slice : 
    Prelude.unit ->
    FA.slice ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__state_passing_loop : 
    Prelude.unit ->
    FA.state_passing_loop ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__trait_item_default : 
    Prelude.unit ->
    FA.trait_item_default ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__unsafe : 
    Prelude.unit ->
    FA.unsafe ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__while_loop : 
    Prelude.unit ->
    FA.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(FA).arm ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_arm' : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).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(FA).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(FA).borrow_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(FA).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(FA).expr ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_expr' : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).expr' ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_field_pat : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).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(FA).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(FA).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(FA).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(FA).generic_value ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_generics : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).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(FA).guard ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_guard' : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).guard' ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_impl_expr : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).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(FA).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(FA).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(FA).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(FA).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(FA).item ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_item' : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).item' ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_lhs : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).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(FA).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(FA).loop_state ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_modul : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).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(FA).param ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_pat : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).pat ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_pat' : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).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(FA).projection_predicate ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_quote : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).quote ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_safety_kind : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).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(FA).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(FA).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(FA).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(FA).trait_item' ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_ty : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).ty ->
    (Ast.Global_ident.t, Ast.Global_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_variant : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).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 ->
    FA.arbitrary_lhs ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__as_pattern : 
    Prelude.unit ->
    FA.as_pattern ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__block : 
    Prelude.unit ->
    FA.block ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__break : 
    Prelude.unit ->
    FA.break ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__construct_base : 
    Prelude.unit ->
    FA.construct_base ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__continue : 
    Prelude.unit ->
    FA.continue ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__dyn : 
    Prelude.unit ->
    FA.dyn ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__early_exit : 
    Prelude.unit ->
    FA.early_exit ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__for_index_loop : 
    Prelude.unit ->
    FA.for_index_loop ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__for_loop : 
    Prelude.unit ->
    FA.for_loop ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__lifetime : 
    Prelude.unit ->
    FA.lifetime ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__loop : 
    Prelude.unit ->
    FA.loop ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__macro : 
    Prelude.unit ->
    FA.macro ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__match_guard : 
    Prelude.unit ->
    FA.match_guard ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__monadic_action : 
    Prelude.unit ->
    FA.monadic_action ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__monadic_binding : 
    Prelude.unit ->
    FA.monadic_binding ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__mutable_pointer : 
    Prelude.unit ->
    FA.mutable_pointer ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__mutable_reference : 
    Prelude.unit ->
    FA.mutable_reference ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__mutable_variable : 
    Prelude.unit ->
    FA.mutable_variable ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__nontrivial_lhs : 
    Prelude.unit ->
    FA.nontrivial_lhs ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__question_mark : 
    Prelude.unit ->
    FA.question_mark ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__raw_pointer : 
    Prelude.unit ->
    FA.raw_pointer ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__reference : 
    Prelude.unit ->
    FA.reference ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__slice : 
    Prelude.unit ->
    FA.slice ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__state_passing_loop : 
    Prelude.unit ->
    FA.state_passing_loop ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__trait_item_default : 
    Prelude.unit ->
    FA.trait_item_default ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__unsafe : 
    Prelude.unit ->
    FA.unsafe ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__while_loop : 
    Prelude.unit ->
    FA.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(FA).arm ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_arm' : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).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(FA).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(FA).borrow_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(FA).dyn_trait_goal ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_expr : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).expr ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_expr' : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).expr' ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_field_pat : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).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(FA).generic_constraint ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_generic_param : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).generic_param ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_generic_param_kind : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).generic_param_kind ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_generic_value : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).generic_value ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_generics : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).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(FA).guard ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_guard' : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).guard' ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_impl_expr : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).impl_expr ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_impl_expr_kind : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).impl_expr_kind ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_impl_ident : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).impl_ident ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_impl_item : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).impl_item ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_impl_item' : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).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(FA).item ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_item' : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).item' ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_lhs : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).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(FA).loop_kind ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_loop_state : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).loop_state ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_modul : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).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(FA).param ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_pat : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).pat ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_pat' : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).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(FA).projection_predicate ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_quote : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).quote ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_safety_kind : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).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(FA).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(FA).trait_goal ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_trait_item : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).trait_item ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_trait_item' : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).trait_item' ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_ty : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).ty ->
    (Concrete_ident.t, Concrete_ident.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_variant : 
    Prelude.unit ->
    Hax_engine__Ast.Make(FA).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 : 
  (FA.arbitrary_lhs -> AST.expr -> Sets.TypedLocalIdent.t) ->
  < visit_F__arbitrary_lhs : 
    unit ->
    FA.arbitrary_lhs ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__as_pattern : 
    unit ->
    FA.as_pattern ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__block : 
    unit ->
    FA.block ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__break : 
    unit ->
    FA.break ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__construct_base : 
    unit ->
    FA.construct_base ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__continue : 
    unit ->
    FA.continue ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__dyn : 
    unit ->
    FA.dyn ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__early_exit : 
    unit ->
    FA.early_exit ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__for_index_loop : 
    unit ->
    FA.for_index_loop ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__for_loop : 
    unit ->
    FA.for_loop ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__lifetime : 
    unit ->
    FA.lifetime ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__loop : 
    unit ->
    FA.loop ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__macro : 
    unit ->
    FA.macro ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__match_guard : 
    unit ->
    FA.match_guard ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__monadic_action : 
    unit ->
    FA.monadic_action ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__monadic_binding : 
    unit ->
    FA.monadic_binding ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__mutable_pointer : 
    unit ->
    FA.mutable_pointer ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__mutable_reference : 
    unit ->
    FA.mutable_reference ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__mutable_variable : 
    unit ->
    FA.mutable_variable ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__nontrivial_lhs : 
    unit ->
    FA.nontrivial_lhs ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__question_mark : 
    unit ->
    FA.question_mark ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__raw_pointer : 
    unit ->
    FA.raw_pointer ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__reference : 
    unit ->
    FA.reference ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__slice : 
    unit ->
    FA.slice ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__state_passing_loop : 
    unit ->
    FA.state_passing_loop ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__trait_item_default : 
    unit ->
    FA.trait_item_default ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__unsafe : 
    unit ->
    FA.unsafe ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_F__while_loop : 
    unit ->
    FA.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(FA).arm ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_arm' : 
    unit ->
    Hax_engine__Ast.Make(FA).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(FA).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(FA).borrow_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(FA).dyn_trait_goal ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_expr : 
    unit ->
    Hax_engine__Ast.Make(FA).expr ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_expr' : 
    unit ->
    Hax_engine__Ast.Make(FA).expr' ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_field_pat : 
    unit ->
    Hax_engine__Ast.Make(FA).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(FA).generic_constraint ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_generic_param : 
    unit ->
    Hax_engine__Ast.Make(FA).generic_param ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_generic_param_kind : 
    unit ->
    Hax_engine__Ast.Make(FA).generic_param_kind ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_generic_value : 
    unit ->
    Hax_engine__Ast.Make(FA).generic_value ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_generics : 
    unit ->
    Hax_engine__Ast.Make(FA).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(FA).guard ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_guard' : 
    unit ->
    Hax_engine__Ast.Make(FA).guard' ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_impl_expr : 
    unit ->
    Hax_engine__Ast.Make(FA).impl_expr ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_impl_expr_kind : 
    unit ->
    Hax_engine__Ast.Make(FA).impl_expr_kind ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_impl_ident : 
    unit ->
    Hax_engine__Ast.Make(FA).impl_ident ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_impl_item : 
    unit ->
    Hax_engine__Ast.Make(FA).impl_item ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_impl_item' : 
    unit ->
    Hax_engine__Ast.Make(FA).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(FA).item ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_item' : 
    unit ->
    Hax_engine__Ast.Make(FA).item' ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_lhs : 
    unit ->
    Hax_engine__Ast.Make(FA).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(FA).loop_kind ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_loop_state : 
    unit ->
    Hax_engine__Ast.Make(FA).loop_state ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_modul : 
    unit ->
    Hax_engine__Ast.Make(FA).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(FA).param ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_pat : 
    unit ->
    Hax_engine__Ast.Make(FA).pat ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_pat' : 
    unit ->
    Hax_engine__Ast.Make(FA).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(FA).projection_predicate ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_quote : 
    unit ->
    Hax_engine__Ast.Make(FA).quote ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_safety_kind : 
    unit ->
    Hax_engine__Ast.Make(FA).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(FA).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(FA).trait_goal ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_trait_item : 
    unit ->
    Hax_engine__Ast.Make(FA).trait_item ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_trait_item' : 
    unit ->
    Hax_engine__Ast.Make(FA).trait_item' ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_ty : 
    unit ->
    Hax_engine__Ast.Make(FA).ty ->
    (TypedLocalIdent.t, TypedLocalIdent.comparator_witness)
      Hax_engine.Prelude.Set.t
  ; visit_variant : 
    unit ->
    Hax_engine__Ast.Make(FA).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 ->
    FA.arbitrary_lhs ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__as_pattern : 
    unit ->
    FA.as_pattern ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__block : unit -> FA.block -> AST.expr Hax_engine.Prelude.List.t
  ; visit_F__break : unit -> FA.break -> AST.expr Hax_engine.Prelude.List.t
  ; visit_F__construct_base : 
    unit ->
    FA.construct_base ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__continue : 
    unit ->
    FA.continue ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__dyn : unit -> FA.dyn -> AST.expr Hax_engine.Prelude.List.t
  ; visit_F__early_exit : 
    unit ->
    FA.early_exit ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__for_index_loop : 
    unit ->
    FA.for_index_loop ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__for_loop : 
    unit ->
    FA.for_loop ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__lifetime : 
    unit ->
    FA.lifetime ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__loop : unit -> FA.loop -> AST.expr Hax_engine.Prelude.List.t
  ; visit_F__macro : unit -> FA.macro -> AST.expr Hax_engine.Prelude.List.t
  ; visit_F__match_guard : 
    unit ->
    FA.match_guard ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__monadic_action : 
    unit ->
    FA.monadic_action ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__monadic_binding : 
    unit ->
    FA.monadic_binding ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__mutable_pointer : 
    unit ->
    FA.mutable_pointer ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__mutable_reference : 
    unit ->
    FA.mutable_reference ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__mutable_variable : 
    unit ->
    FA.mutable_variable ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__nontrivial_lhs : 
    unit ->
    FA.nontrivial_lhs ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__question_mark : 
    unit ->
    FA.question_mark ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__raw_pointer : 
    unit ->
    FA.raw_pointer ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__reference : 
    unit ->
    FA.reference ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__slice : unit -> FA.slice -> AST.expr Hax_engine.Prelude.List.t
  ; visit_F__state_passing_loop : 
    unit ->
    FA.state_passing_loop ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__trait_item_default : 
    unit ->
    FA.trait_item_default ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_F__unsafe : unit -> FA.unsafe -> AST.expr Hax_engine.Prelude.List.t
  ; visit_F__while_loop : 
    unit ->
    FA.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(FA).arm ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_arm' : 
    unit ->
    Hax_engine__Ast.Make(FA).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(FA).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(FA).borrow_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(FA).dyn_trait_goal ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_expr : 
    unit ->
    Hax_engine__Ast.Make(FA).expr ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_expr' : 
    unit ->
    Hax_engine__Ast.Make(FA).expr' ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_field_pat : 
    unit ->
    Hax_engine__Ast.Make(FA).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(FA).generic_constraint ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_generic_param : 
    unit ->
    Hax_engine__Ast.Make(FA).generic_param ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_generic_param_kind : 
    unit ->
    Hax_engine__Ast.Make(FA).generic_param_kind ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_generic_value : 
    unit ->
    Hax_engine__Ast.Make(FA).generic_value ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_generics : 
    unit ->
    Hax_engine__Ast.Make(FA).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(FA).guard ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_guard' : 
    unit ->
    Hax_engine__Ast.Make(FA).guard' ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_impl_expr : 
    unit ->
    Hax_engine__Ast.Make(FA).impl_expr ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_impl_expr_kind : 
    unit ->
    Hax_engine__Ast.Make(FA).impl_expr_kind ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_impl_ident : 
    unit ->
    Hax_engine__Ast.Make(FA).impl_ident ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_impl_item : 
    unit ->
    Hax_engine__Ast.Make(FA).impl_item ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_impl_item' : 
    unit ->
    Hax_engine__Ast.Make(FA).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(FA).item ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_item' : 
    unit ->
    Hax_engine__Ast.Make(FA).item' ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_lhs : 
    unit ->
    Hax_engine__Ast.Make(FA).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(FA).loop_kind ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_loop_state : 
    unit ->
    Hax_engine__Ast.Make(FA).loop_state ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_modul : 
    unit ->
    Hax_engine__Ast.Make(FA).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(FA).param ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_pat : 
    unit ->
    Hax_engine__Ast.Make(FA).pat ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_pat' : 
    unit ->
    Hax_engine__Ast.Make(FA).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(FA).projection_predicate ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_quote : 
    unit ->
    Hax_engine__Ast.Make(FA).quote ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_safety_kind : 
    unit ->
    Hax_engine__Ast.Make(FA).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(FA).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(FA).trait_goal ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_trait_item : 
    unit ->
    Hax_engine__Ast.Make(FA).trait_item ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_trait_item' : 
    unit ->
    Hax_engine__Ast.Make(FA).trait_item' ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_ty : 
    unit ->
    Hax_engine__Ast.Make(FA).ty ->
    AST.expr Hax_engine.Prelude.List.t
  ; visit_variant : 
    unit ->
    Hax_engine__Ast.Make(FA).variant ->
    AST.expr Hax_engine.Prelude.List.t >