fstar 2022.01.15 · OCaml Package

type (!'a, !'b, !'rua, !'rub, !'dummyV0, !'dummyV1) lex_t =

| Left_lex of 'a * 'a * 'b * 'b * 'rua
| Right_lex of 'a * 'b * 'b * 'rub

val uu___is_Left_lex : 
  ('a, 'b) Prims.dtuple2 ->
  ('a, 'b) Prims.dtuple2 ->
  ('a, 'b, 'rua, 'rub, Prims.unit, Prims.unit) lex_t ->
  Prims.bool

val __proj__Left_lex__item__x1 : 
  ('a, 'b) Prims.dtuple2 ->
  ('a, 'b) Prims.dtuple2 ->
  ('a, 'b, 'rua, 'rub, Prims.unit, Prims.unit) lex_t ->
  'a

val __proj__Left_lex__item__x2 : 
  ('a, 'b) Prims.dtuple2 ->
  ('a, 'b) Prims.dtuple2 ->
  ('a, 'b, 'rua, 'rub, Prims.unit, Prims.unit) lex_t ->
  'a

val __proj__Left_lex__item__y1 : 
  ('a, 'b) Prims.dtuple2 ->
  ('a, 'b) Prims.dtuple2 ->
  ('a, 'b, 'rua, 'rub, Prims.unit, Prims.unit) lex_t ->
  'b

val __proj__Left_lex__item__y2 : 
  ('a, 'b) Prims.dtuple2 ->
  ('a, 'b) Prims.dtuple2 ->
  ('a, 'b, 'rua, 'rub, Prims.unit, Prims.unit) lex_t ->
  'b

val __proj__Left_lex__item___4 : 
  ('a, 'b) Prims.dtuple2 ->
  ('a, 'b) Prims.dtuple2 ->
  ('a, 'b, 'rua, 'rub, Prims.unit, Prims.unit) lex_t ->
  'rua

val uu___is_Right_lex : 
  ('a, 'b) Prims.dtuple2 ->
  ('a, 'b) Prims.dtuple2 ->
  ('a, 'b, 'rua, 'rub, Prims.unit, Prims.unit) lex_t ->
  Prims.bool

val __proj__Right_lex__item__x : 
  ('a, 'b) Prims.dtuple2 ->
  ('a, 'b) Prims.dtuple2 ->
  ('a, 'b, 'rua, 'rub, Prims.unit, Prims.unit) lex_t ->
  'a

val __proj__Right_lex__item__y1 : 
  ('a, 'b) Prims.dtuple2 ->
  ('a, 'b) Prims.dtuple2 ->
  ('a, 'b, 'rua, 'rub, Prims.unit, Prims.unit) lex_t ->
  'b

val __proj__Right_lex__item__y2 : 
  ('a, 'b) Prims.dtuple2 ->
  ('a, 'b) Prims.dtuple2 ->
  ('a, 'b, 'rua, 'rub, Prims.unit, Prims.unit) lex_t ->
  'b

val __proj__Right_lex__item___3 : 
  ('a, 'b) Prims.dtuple2 ->
  ('a, 'b) Prims.dtuple2 ->
  ('a, 'b, 'rua, 'rub, Prims.unit, Prims.unit) lex_t ->
  'rub

val lex_t_wf_aux : 
  'a ->
  ('a, 'rua, Prims.unit) FStar_WellFounded.acc ->
  ('a -> ('b, 'rub) FStar_WellFounded.well_founded) ->
  'b ->
  ('b, 'rub, Prims.unit) FStar_WellFounded.acc ->
  ('a, 'b) Prims.dtuple2 ->
  ('a, 'b, 'rua, 'rub, Prims.unit, Prims.unit) lex_t ->
  (('a, 'b) Prims.dtuple2,
    ('a, 'b, 'rua, 'rub, Prims.unit, Prims.unit) lex_t,
    Prims.unit)
    FStar_WellFounded.acc

val lex_t_wf : 
  ('uuuuu, 'uuuuu2) FStar_WellFounded.well_founded ->
  ('uuuuu -> ('uuuuu1, 'uuuuu3) FStar_WellFounded.well_founded) ->
  (('uuuuu, 'uuuuu1) Prims.dtuple2,
    ('uuuuu, 'uuuuu1, 'uuuuu2, 'uuuuu3, Prims.unit, Prims.unit) lex_t)
    FStar_WellFounded.well_founded

type ('a, 'b, 'rua, 'rub, 'uuuuu, 'uuuuu1) lex_aux = Obj.t

type ('a, 'b, 'rua, 'rub, 'wfua, 'wfub, 'uuuuu, 'uuuuu1) lex = Obj.t

val tuple_to_dep_tuple : ('a * 'b) -> ('a, 'b) Prims.dtuple2

type (!'a, !'b, !'rua, !'rub, 'x, 'y) lex_t_non_dep =
  ('a, 'b, 'rua, 'rub, Prims.unit, Prims.unit) lex_t

val lex_t_non_dep_wf : 
  ('a, 'rua) FStar_WellFounded.well_founded ->
  ('b, 'rub) FStar_WellFounded.well_founded ->
  ('a * 'b, ('a, 'b, 'rua, 'rub, Prims.unit, Prims.unit) lex_t)
    FStar_WellFounded.well_founded

type (!'a, !'b, !'rua, !'rub, !'dummyV0, !'dummyV1) sym =

| Left_sym of 'a * 'a * 'b * 'rua
| Right_sym of 'a * 'b * 'b * 'rub

val uu___is_Left_sym : 
  ('a * 'b) ->
  ('a * 'b) ->
  ('a, 'b, 'rua, 'rub, Prims.unit, Prims.unit) sym ->
  Prims.bool

val __proj__Left_sym__item__x1 : 
  ('a * 'b) ->
  ('a * 'b) ->
  ('a, 'b, 'rua, 'rub, Prims.unit, Prims.unit) sym ->
  'a

val __proj__Left_sym__item__x2 : 
  ('a * 'b) ->
  ('a * 'b) ->
  ('a, 'b, 'rua, 'rub, Prims.unit, Prims.unit) sym ->
  'a

val __proj__Left_sym__item__y : 
  ('a * 'b) ->
  ('a * 'b) ->
  ('a, 'b, 'rua, 'rub, Prims.unit, Prims.unit) sym ->
  'b

val __proj__Left_sym__item___3 : 
  ('a * 'b) ->
  ('a * 'b) ->
  ('a, 'b, 'rua, 'rub, Prims.unit, Prims.unit) sym ->
  'rua

val uu___is_Right_sym : 
  ('a * 'b) ->
  ('a * 'b) ->
  ('a, 'b, 'rua, 'rub, Prims.unit, Prims.unit) sym ->
  Prims.bool

val __proj__Right_sym__item__x : 
  ('a * 'b) ->
  ('a * 'b) ->
  ('a, 'b, 'rua, 'rub, Prims.unit, Prims.unit) sym ->
  'a

val __proj__Right_sym__item__y1 : 
  ('a * 'b) ->
  ('a * 'b) ->
  ('a, 'b, 'rua, 'rub, Prims.unit, Prims.unit) sym ->
  'b

val __proj__Right_sym__item__y2 : 
  ('a * 'b) ->
  ('a * 'b) ->
  ('a, 'b, 'rua, 'rub, Prims.unit, Prims.unit) sym ->
  'b

val __proj__Right_sym__item___3 : 
  ('a * 'b) ->
  ('a * 'b) ->
  ('a, 'b, 'rua, 'rub, Prims.unit, Prims.unit) sym ->
  'rub

val sym_sub_lex : 
  ('a * 'b) ->
  ('a * 'b) ->
  ('a, 'b, 'rua, 'rub, Prims.unit, Prims.unit) sym ->
  ('a, 'b, 'rua, 'rub, Prims.unit, Prims.unit) lex_t

val sym_wf : 
  ('a, 'rua) FStar_WellFounded.well_founded ->
  ('b, 'rub) FStar_WellFounded.well_founded ->
  ('a * 'b, ('a, 'b, 'rua, 'rub, Prims.unit, Prims.unit) sym)
    FStar_WellFounded.well_founded