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