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