fstar 2025.02.17 · 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

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

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

package fstar