open Preamble

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Exp

open Arithmetic

open Vector

open Div_and_mod

open Util

open FoldStuff

open BitVector

open Jmeq

open Russell

open List

open Setoids

open Monad

open Option

open Extranat

open Bool

open Relations

open Nat

open Integers

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Lists

open Positive

open Identifiers

type ident = PreIdentifiers.identifier

val ident_eq : ident -> ident -> (__, __) Types.sum

val ident_of_nat : Nat.nat -> ident

type region =
| XData
| Code

val region_rect_Type4 : 'a1 -> 'a1 -> region -> 'a1

val region_rect_Type5 : 'a1 -> 'a1 -> region -> 'a1

val region_rect_Type3 : 'a1 -> 'a1 -> region -> 'a1

val region_rect_Type2 : 'a1 -> 'a1 -> region -> 'a1

val region_rect_Type1 : 'a1 -> 'a1 -> region -> 'a1

val region_rect_Type0 : 'a1 -> 'a1 -> region -> 'a1

val region_inv_rect_Type4 : region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val region_inv_rect_Type3 : region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val region_inv_rect_Type2 : region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val region_inv_rect_Type1 : region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val region_inv_rect_Type0 : region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val region_discr : region -> region -> __

val region_jmdiscr : region -> region -> __

val eq_region : region -> region -> Bool.bool

val eq_region_elim : region -> region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val eq_region_dec : region -> region -> (__, __) Types.sum

val size_pointer : Nat.nat

type signedness =
| Signed
| Unsigned

val signedness_rect_Type4 : 'a1 -> 'a1 -> signedness -> 'a1

val signedness_rect_Type5 : 'a1 -> 'a1 -> signedness -> 'a1

val signedness_rect_Type3 : 'a1 -> 'a1 -> signedness -> 'a1

val signedness_rect_Type2 : 'a1 -> 'a1 -> signedness -> 'a1

val signedness_rect_Type1 : 'a1 -> 'a1 -> signedness -> 'a1

val signedness_rect_Type0 : 'a1 -> 'a1 -> signedness -> 'a1

val signedness_inv_rect_Type4 :
  signedness -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val signedness_inv_rect_Type3 :
  signedness -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val signedness_inv_rect_Type2 :
  signedness -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val signedness_inv_rect_Type1 :
  signedness -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val signedness_inv_rect_Type0 :
  signedness -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val signedness_discr : signedness -> signedness -> __

val signedness_jmdiscr : signedness -> signedness -> __

type intsize =
| I8
| I16
| I32

val intsize_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1

val intsize_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1

val intsize_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1

val intsize_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1

val intsize_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1

val intsize_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1

val intsize_inv_rect_Type4 :
  intsize -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val intsize_inv_rect_Type3 :
  intsize -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val intsize_inv_rect_Type2 :
  intsize -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val intsize_inv_rect_Type1 :
  intsize -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val intsize_inv_rect_Type0 :
  intsize -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val intsize_discr : intsize -> intsize -> __

val intsize_jmdiscr : intsize -> intsize -> __

type floatsize =
| F32
| F64

val floatsize_rect_Type4 : 'a1 -> 'a1 -> floatsize -> 'a1

val floatsize_rect_Type5 : 'a1 -> 'a1 -> floatsize -> 'a1

val floatsize_rect_Type3 : 'a1 -> 'a1 -> floatsize -> 'a1

val floatsize_rect_Type2 : 'a1 -> 'a1 -> floatsize -> 'a1

val floatsize_rect_Type1 : 'a1 -> 'a1 -> floatsize -> 'a1

val floatsize_rect_Type0 : 'a1 -> 'a1 -> floatsize -> 'a1

val floatsize_inv_rect_Type4 : floatsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val floatsize_inv_rect_Type3 : floatsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val floatsize_inv_rect_Type2 : floatsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val floatsize_inv_rect_Type1 : floatsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val floatsize_inv_rect_Type0 : floatsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val floatsize_discr : floatsize -> floatsize -> __

val floatsize_jmdiscr : floatsize -> floatsize -> __

type typ =
| ASTint of intsize * signedness
| ASTptr

val typ_rect_Type4 : (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1

val typ_rect_Type5 : (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1

val typ_rect_Type3 : (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1

val typ_rect_Type2 : (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1

val typ_rect_Type1 : (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1

val typ_rect_Type0 : (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1

val typ_inv_rect_Type4 :
  typ -> (intsize -> signedness -> __ -> 'a1) -> (__ -> 'a1) -> 'a1

val typ_inv_rect_Type3 :
  typ -> (intsize -> signedness -> __ -> 'a1) -> (__ -> 'a1) -> 'a1

val typ_inv_rect_Type2 :
  typ -> (intsize -> signedness -> __ -> 'a1) -> (__ -> 'a1) -> 'a1

val typ_inv_rect_Type1 :
  typ -> (intsize -> signedness -> __ -> 'a1) -> (__ -> 'a1) -> 'a1

val typ_inv_rect_Type0 :
  typ -> (intsize -> signedness -> __ -> 'a1) -> (__ -> 'a1) -> 'a1

val typ_discr : typ -> typ -> __

val typ_jmdiscr : typ -> typ -> __

type sigType = typ

val sigType_Int : typ

val sigType_Ptr : typ

val pred_size_intsize : intsize -> Nat.nat

val size_intsize : intsize -> Nat.nat

val bitsize_of_intsize : intsize -> Nat.nat

val eq_intsize : intsize -> intsize -> Bool.bool

val eq_intsize_elim : intsize -> intsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val signedness_check : signedness -> signedness -> 'a1 -> 'a1 -> 'a1

val inttyp_eq_elim' :
  intsize -> intsize -> signedness -> signedness -> 'a1 -> 'a1 -> 'a1

val intsize_eq_elim' : intsize -> intsize -> 'a1 -> 'a1 -> 'a1

val intsize_eq_elim : intsize -> intsize -> 'a2 -> ('a2 -> 'a1) -> 'a1 -> 'a1

val intsize_eq_elim_elim :
  intsize -> intsize -> 'a2 -> ('a2 -> 'a1) -> 'a1 -> (__ -> 'a3) -> (__ ->
  __) -> 'a3

type bvint = BitVector.bitVector

val repr : intsize -> Nat.nat -> bvint

val size_floatsize : floatsize -> Nat.nat

val floatsize_eq_elim : floatsize -> floatsize -> 'a1 -> 'a1 -> 'a1

val typesize : typ -> Nat.nat

val typ_eq : typ -> typ -> (__, __) Types.sum

val opt_typ_eq : typ Types.option -> typ Types.option -> (__, __) Types.sum

type signature = { sig_args : typ List.list; sig_res : typ Types.option }

val signature_rect_Type4 :
  (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1

val signature_rect_Type5 :
  (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1

val signature_rect_Type3 :
  (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1

val signature_rect_Type2 :
  (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1

val signature_rect_Type1 :
  (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1

val signature_rect_Type0 :
  (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1

val sig_args : signature -> typ List.list

val sig_res : signature -> typ Types.option

val signature_inv_rect_Type4 :
  signature -> (typ List.list -> typ Types.option -> __ -> 'a1) -> 'a1

val signature_inv_rect_Type3 :
  signature -> (typ List.list -> typ Types.option -> __ -> 'a1) -> 'a1

val signature_inv_rect_Type2 :
  signature -> (typ List.list -> typ Types.option -> __ -> 'a1) -> 'a1

val signature_inv_rect_Type1 :
  signature -> (typ List.list -> typ Types.option -> __ -> 'a1) -> 'a1

val signature_inv_rect_Type0 :
  signature -> (typ List.list -> typ Types.option -> __ -> 'a1) -> 'a1

val signature_discr : signature -> signature -> __

val signature_jmdiscr : signature -> signature -> __

type signature0 = signature

val signature_args : signature -> typ List.list

val signature_return : signature -> typ Types.option

val proj_sig_res : signature -> typ

type init_data =
| Init_int8 of bvint
| Init_int16 of bvint
| Init_int32 of bvint
| Init_space of Nat.nat
| Init_null
| Init_addrof of ident * Nat.nat

val init_data_rect_Type4 :
  (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Nat.nat -> 'a1) ->
  'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1

val init_data_rect_Type5 :
  (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Nat.nat -> 'a1) ->
  'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1

val init_data_rect_Type3 :
  (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Nat.nat -> 'a1) ->
  'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1

val init_data_rect_Type2 :
  (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Nat.nat -> 'a1) ->
  'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1

val init_data_rect_Type1 :
  (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Nat.nat -> 'a1) ->
  'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1

val init_data_rect_Type0 :
  (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Nat.nat -> 'a1) ->
  'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1

val init_data_inv_rect_Type4 :
  init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
  -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat -> __
  -> 'a1) -> 'a1

val init_data_inv_rect_Type3 :
  init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
  -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat -> __
  -> 'a1) -> 'a1

val init_data_inv_rect_Type2 :
  init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
  -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat -> __
  -> 'a1) -> 'a1

val init_data_inv_rect_Type1 :
  init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
  -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat -> __
  -> 'a1) -> 'a1

val init_data_inv_rect_Type0 :
  init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
  -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat -> __
  -> 'a1) -> 'a1

val init_data_discr : init_data -> init_data -> __

val init_data_jmdiscr : init_data -> init_data -> __

type ('f, 'v) program = { prog_vars : ((ident, region) Types.prod, 'v)
                                      Types.prod List.list;
                          prog_funct : (ident, 'f) Types.prod List.list;
                          prog_main : ident }

val program_rect_Type4 :
  (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
  Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3

val program_rect_Type5 :
  (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
  Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3

val program_rect_Type3 :
  (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
  Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3

val program_rect_Type2 :
  (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
  Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3

val program_rect_Type1 :
  (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
  Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3

val program_rect_Type0 :
  (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
  Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3

val prog_vars :
  ('a1, 'a2) program -> ((ident, region) Types.prod, 'a2) Types.prod
  List.list

val prog_funct : ('a1, 'a2) program -> (ident, 'a1) Types.prod List.list

val prog_main : ('a1, 'a2) program -> ident

val program_inv_rect_Type4 :
  ('a1, 'a2) program -> (((ident, region) Types.prod, 'a2) Types.prod
  List.list -> (ident, 'a1) Types.prod List.list -> ident -> __ -> 'a3) ->
  'a3

val program_inv_rect_Type3 :
  ('a1, 'a2) program -> (((ident, region) Types.prod, 'a2) Types.prod
  List.list -> (ident, 'a1) Types.prod List.list -> ident -> __ -> 'a3) ->
  'a3

val program_inv_rect_Type2 :
  ('a1, 'a2) program -> (((ident, region) Types.prod, 'a2) Types.prod
  List.list -> (ident, 'a1) Types.prod List.list -> ident -> __ -> 'a3) ->
  'a3

val program_inv_rect_Type1 :
  ('a1, 'a2) program -> (((ident, region) Types.prod, 'a2) Types.prod
  List.list -> (ident, 'a1) Types.prod List.list -> ident -> __ -> 'a3) ->
  'a3

val program_inv_rect_Type0 :
  ('a1, 'a2) program -> (((ident, region) Types.prod, 'a2) Types.prod
  List.list -> (ident, 'a1) Types.prod List.list -> ident -> __ -> 'a3) ->
  'a3

val program_discr : ('a1, 'a2) program -> ('a1, 'a2) program -> __

val program_jmdiscr : ('a1, 'a2) program -> ('a1, 'a2) program -> __

val prog_funct_names : ('a1, 'a2) program -> ident List.list

val prog_var_names : ('a1, 'a2) program -> ident List.list

val transf_program :
  ('a1 -> 'a2) -> (ident, 'a1) Types.prod List.list -> (ident, 'a2)
  Types.prod List.list

val transform_program :
  ('a1, 'a3) program -> (ident List.list -> 'a1 -> 'a2) -> ('a2, 'a3) program

val transf_program_gen :
  PreIdentifiers.identifierTag -> Identifiers.universe ->
  (Identifiers.universe -> 'a1 -> ('a2, Identifiers.universe) Types.prod) ->
  (ident, 'a1) Types.prod List.list -> ((ident, 'a2) Types.prod List.list,
  Identifiers.universe) Types.prod

val transform_program_gen :
  PreIdentifiers.identifierTag -> Identifiers.universe -> ('a1, 'a3) program
  -> (ident List.list -> Identifiers.universe -> 'a1 -> ('a2,
  Identifiers.universe) Types.prod) -> (('a2, 'a3) program,
  Identifiers.universe) Types.prod

val map_partial :
  ('a2 -> 'a3 Errors.res) -> ('a1, 'a2) Types.prod List.list -> ('a1, 'a3)
  Types.prod List.list Errors.res

val transform_partial_program :
  ('a1, 'a3) program -> (ident List.list -> 'a1 -> 'a2 Errors.res) -> ('a2,
  'a3) program Errors.res

val transform_partial_program2 :
  ('a1, 'a3) program -> (ident List.list -> 'a1 -> 'a2 Errors.res) -> ('a3 ->
  'a4 Errors.res) -> ('a2, 'a4) program Errors.res

type matching =
| Mk_matching

val matching_rect_Type4 :
  (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1

val matching_rect_Type5 :
  (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1

val matching_rect_Type3 :
  (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1

val matching_rect_Type2 :
  (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1

val matching_rect_Type1 :
  (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1

val matching_rect_Type0 :
  (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1

type m_A 

type m_B 

type m_V 

type m_W 

val matching_inv_rect_Type4 :
  matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val matching_inv_rect_Type3 :
  matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val matching_inv_rect_Type2 :
  matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val matching_inv_rect_Type1 :
  matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val matching_inv_rect_Type0 :
  matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val matching_jmdiscr : matching -> matching -> __

val mfe_cast_fn_type :
  matching -> ident List.list -> ident List.list -> __ -> __

val match_program_rect_Type4 :
  matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> 'a1)
  -> 'a1

val match_program_rect_Type5 :
  matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> 'a1)
  -> 'a1

val match_program_rect_Type3 :
  matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> 'a1)
  -> 'a1

val match_program_rect_Type2 :
  matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> 'a1)
  -> 'a1

val match_program_rect_Type1 :
  matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> 'a1)
  -> 'a1

val match_program_rect_Type0 :
  matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> 'a1)
  -> 'a1

val match_program_inv_rect_Type4 :
  matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
  -> 'a1) -> 'a1

val match_program_inv_rect_Type3 :
  matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
  -> 'a1) -> 'a1

val match_program_inv_rect_Type2 :
  matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
  -> 'a1) -> 'a1

val match_program_inv_rect_Type1 :
  matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
  -> 'a1) -> 'a1

val match_program_inv_rect_Type0 :
  matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
  -> 'a1) -> 'a1

val match_program_discr :
  matching -> (__, __) program -> (__, __) program -> __

val match_program_jmdiscr :
  matching -> (__, __) program -> (__, __) program -> __

type external_function = { ef_id : ident; ef_sig : signature }

val external_function_rect_Type4 :
  (ident -> signature -> 'a1) -> external_function -> 'a1

val external_function_rect_Type5 :
  (ident -> signature -> 'a1) -> external_function -> 'a1

val external_function_rect_Type3 :
  (ident -> signature -> 'a1) -> external_function -> 'a1

val external_function_rect_Type2 :
  (ident -> signature -> 'a1) -> external_function -> 'a1

val external_function_rect_Type1 :
  (ident -> signature -> 'a1) -> external_function -> 'a1

val external_function_rect_Type0 :
  (ident -> signature -> 'a1) -> external_function -> 'a1

val ef_id : external_function -> ident

val ef_sig : external_function -> signature

val external_function_inv_rect_Type4 :
  external_function -> (ident -> signature -> __ -> 'a1) -> 'a1

val external_function_inv_rect_Type3 :
  external_function -> (ident -> signature -> __ -> 'a1) -> 'a1

val external_function_inv_rect_Type2 :
  external_function -> (ident -> signature -> __ -> 'a1) -> 'a1

val external_function_inv_rect_Type1 :
  external_function -> (ident -> signature -> __ -> 'a1) -> 'a1

val external_function_inv_rect_Type0 :
  external_function -> (ident -> signature -> __ -> 'a1) -> 'a1

val external_function_discr : external_function -> external_function -> __

val external_function_jmdiscr : external_function -> external_function -> __

type externalFunction = external_function

val external_function_tag : external_function -> ident

val external_function_sig : external_function -> signature

type 'f fundef =
| Internal of 'f
| External of external_function

val fundef_rect_Type4 :
  ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2

val fundef_rect_Type5 :
  ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2

val fundef_rect_Type3 :
  ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2

val fundef_rect_Type2 :
  ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2

val fundef_rect_Type1 :
  ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2

val fundef_rect_Type0 :
  ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2

val fundef_inv_rect_Type4 :
  'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) -> 'a2

val fundef_inv_rect_Type3 :
  'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) -> 'a2

val fundef_inv_rect_Type2 :
  'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) -> 'a2

val fundef_inv_rect_Type1 :
  'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) -> 'a2

val fundef_inv_rect_Type0 :
  'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) -> 'a2

val fundef_discr : 'a1 fundef -> 'a1 fundef -> __

val fundef_jmdiscr : 'a1 fundef -> 'a1 fundef -> __

val transf_fundef : ('a1 -> 'a2) -> 'a1 fundef -> 'a2 fundef

val transf_partial_fundef :
  ('a1 -> 'a2 Errors.res) -> 'a1 fundef -> 'a2 fundef Errors.res