fstar 2022.01.15 · OCaml Package

val dump : 
  Prims.string ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

type var = Prims.nat

type exp =

| Unit
| Var of var
| Mult of exp * exp

val uu___is_Unit : exp -> Prims.bool

val uu___is_Var : exp -> Prims.bool

val __proj__Var__item___0 : exp -> var

val uu___is_Mult : exp -> Prims.bool

val __proj__Mult__item___0 : exp -> exp

val __proj__Mult__item___1 : exp -> exp

val exp_to_string : exp -> Prims.string

type (!'a, !'b) vmap = (var * ('a * 'b)) Prims.list * ('a * 'b)

val const : 'a -> 'b -> ('a, 'b) vmap

val select : var -> ('a, 'b) vmap -> 'a

val select_extra : var -> ('a, 'b) vmap -> 'b

val update : var -> 'a -> 'b -> ('a, 'b) vmap -> ('a, 'b) vmap

val mdenote : 'a FStar_Algebra_CommMonoid.cm -> ('a, 'b) vmap -> exp -> 'a

val xsdenote : 
  'a FStar_Algebra_CommMonoid.cm ->
  ('a, 'b) vmap ->
  var Prims.list ->
  'a

val flatten : exp -> var Prims.list

type !'b permute =
  Prims.unit ->
  (Obj.t, 'b) vmap ->
  var Prims.list ->
  var Prims.list

type ('b, 'p) permute_correct = Prims.unit

type ('b, 'p) permute_via_swaps = Prims.unit

val sort : Prims.unit permute

val sortWith : (Prims.nat -> Prims.nat -> Prims.int) -> 'b permute

val canon : ('a, 'b) vmap -> 'b permute -> exp -> var Prims.list

val where_aux : 
  Prims.nat ->
  FStar_Reflection_Types.term ->
  FStar_Reflection_Types.term Prims.list ->
  Prims.nat FStar_Pervasives_Native.option

val where : 
  FStar_Reflection_Types.term ->
  FStar_Reflection_Types.term Prims.list ->
  Prims.nat FStar_Pervasives_Native.option

val reification_aux : 
  (FStar_Reflection_Types.term ->
    FStar_Tactics_Types.proofstate ->
    'a FStar_Tactics_Result.__result) ->
  FStar_Reflection_Types.term Prims.list ->
  ('a, 'b) vmap ->
  (FStar_Reflection_Types.term ->
    FStar_Tactics_Types.proofstate ->
    'b FStar_Tactics_Result.__result) ->
  FStar_Reflection_Types.term ->
  FStar_Reflection_Types.term ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  (exp * FStar_Reflection_Types.term Prims.list * ('a, 'b) vmap)
    FStar_Tactics_Result.__result

val reification : 
  (FStar_Reflection_Types.term ->
    FStar_Tactics_Types.proofstate ->
    'b FStar_Tactics_Result.__result) ->
  'b ->
  Prims.unit ->
  (FStar_Reflection_Types.term ->
    FStar_Tactics_Types.proofstate ->
    Obj.t FStar_Tactics_Result.__result) ->
  (Obj.t ->
    FStar_Tactics_Types.proofstate ->
    FStar_Reflection_Types.term FStar_Tactics_Result.__result) ->
  FStar_Reflection_Types.term ->
  FStar_Reflection_Types.term ->
  Obj.t ->
  FStar_Reflection_Types.term Prims.list ->
  FStar_Tactics_Types.proofstate ->
  (exp Prims.list * (Obj.t, 'b) vmap) FStar_Tactics_Result.__result

val term_mem : 
  FStar_Reflection_Types.term ->
  FStar_Reflection_Types.term Prims.list ->
  Prims.bool

val unfold_topdown : 
  FStar_Reflection_Types.term Prims.list ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val quote_list : 
  FStar_Reflection_Types.term ->
  ('a ->
    FStar_Tactics_Types.proofstate ->
    FStar_Reflection_Types.term FStar_Tactics_Result.__result) ->
  'a Prims.list ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.term FStar_Tactics_Result.__result

val quote_vm : 
  FStar_Reflection_Types.term ->
  FStar_Reflection_Types.term ->
  ('a ->
    FStar_Tactics_Types.proofstate ->
    FStar_Reflection_Types.term FStar_Tactics_Result.__result) ->
  ('b ->
    FStar_Tactics_Types.proofstate ->
    FStar_Reflection_Types.term FStar_Tactics_Result.__result) ->
  ('a, 'b) vmap ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.term FStar_Tactics_Result.__result

val quote_exp : 
  exp ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.term FStar_Tactics_Result.__result

val canon_monoid_aux : 
  FStar_Reflection_Types.term ->
  (FStar_Reflection_Types.term ->
    FStar_Tactics_Types.proofstate ->
    'a FStar_Tactics_Result.__result) ->
  ('a ->
    FStar_Tactics_Types.proofstate ->
    FStar_Reflection_Types.term FStar_Tactics_Result.__result) ->
  FStar_Reflection_Types.term ->
  FStar_Reflection_Types.term ->
  FStar_Reflection_Types.term ->
  'a ->
  FStar_Reflection_Types.term ->
  ('b ->
    FStar_Tactics_Types.proofstate ->
    FStar_Reflection_Types.term FStar_Tactics_Result.__result) ->
  (FStar_Reflection_Types.term ->
    FStar_Tactics_Types.proofstate ->
    'b FStar_Tactics_Result.__result) ->
  'b ->
  FStar_Reflection_Types.term ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val canon_monoid_with : 
  (FStar_Reflection_Types.term ->
    FStar_Tactics_Types.proofstate ->
    'b FStar_Tactics_Result.__result) ->
  'b ->
  'b permute ->
  Prims.unit ->
  Prims.unit ->
  Obj.t FStar_Algebra_CommMonoid.cm ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val canon_monoid : 
  'a FStar_Algebra_CommMonoid.cm ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val is_const : 
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  Prims.bool FStar_Tactics_Result.__result

val const_compare : ('a, Prims.bool) vmap -> var -> var -> Prims.int

val const_last : ('a, Prims.bool) vmap -> var Prims.list -> var Prims.list

val canon_monoid_const : 
  'a FStar_Algebra_CommMonoid.cm ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val is_special : 
  FStar_Reflection_Types.term Prims.list ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  Prims.bool FStar_Tactics_Result.__result

val special_compare : ('a, Prims.bool) vmap -> var -> var -> Prims.int

val special_first : ('a, Prims.bool) vmap -> var Prims.list -> var Prims.list

val canon_monoid_special : 
  FStar_Reflection_Types.term Prims.list ->
  'uuuuu FStar_Algebra_CommMonoid.cm ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result