fstar
  1. Overview
  2. Docs
package fstar
Legend:
Library
Module
Module type
Parameter
Class
Class type
type expr =
  1. | Lit of Prims.int
  2. | Atom of Prims.nat * FStar_Reflection_Types.term
  3. | Plus of expr * expr
  4. | Mult of expr * expr
  5. | Minus of expr * expr
  6. | Land of expr * expr
  7. | Lxor of expr * expr
  8. | Lor of expr * expr
  9. | Ladd of expr * expr
  10. | Lsub of expr * expr
  11. | Shl of expr * expr
  12. | Shr of expr * expr
  13. | Neg of expr
  14. | Udiv of expr * expr
  15. | Umod of expr * expr
  16. | MulMod of expr * expr
  17. | NatToBv of expr
val uu___is_Lit : expr -> Prims.bool
val __proj__Lit__item___0 : expr -> Prims.int
val uu___is_Atom : expr -> Prims.bool
val __proj__Atom__item___0 : expr -> Prims.nat
val __proj__Atom__item___1 : expr -> FStar_Reflection_Types.term
val uu___is_Plus : expr -> Prims.bool
val __proj__Plus__item___0 : expr -> expr
val __proj__Plus__item___1 : expr -> expr
val uu___is_Mult : expr -> Prims.bool
val __proj__Mult__item___0 : expr -> expr
val __proj__Mult__item___1 : expr -> expr
val uu___is_Minus : expr -> Prims.bool
val __proj__Minus__item___0 : expr -> expr
val __proj__Minus__item___1 : expr -> expr
val uu___is_Land : expr -> Prims.bool
val __proj__Land__item___0 : expr -> expr
val __proj__Land__item___1 : expr -> expr
val uu___is_Lxor : expr -> Prims.bool
val __proj__Lxor__item___0 : expr -> expr
val __proj__Lxor__item___1 : expr -> expr
val uu___is_Lor : expr -> Prims.bool
val __proj__Lor__item___0 : expr -> expr
val __proj__Lor__item___1 : expr -> expr
val uu___is_Ladd : expr -> Prims.bool
val __proj__Ladd__item___0 : expr -> expr
val __proj__Ladd__item___1 : expr -> expr
val uu___is_Lsub : expr -> Prims.bool
val __proj__Lsub__item___0 : expr -> expr
val __proj__Lsub__item___1 : expr -> expr
val uu___is_Shl : expr -> Prims.bool
val __proj__Shl__item___0 : expr -> expr
val __proj__Shl__item___1 : expr -> expr
val uu___is_Shr : expr -> Prims.bool
val __proj__Shr__item___0 : expr -> expr
val __proj__Shr__item___1 : expr -> expr
val uu___is_Neg : expr -> Prims.bool
val __proj__Neg__item___0 : expr -> expr
val uu___is_Udiv : expr -> Prims.bool
val __proj__Udiv__item___0 : expr -> expr
val __proj__Udiv__item___1 : expr -> expr
val uu___is_Umod : expr -> Prims.bool
val __proj__Umod__item___0 : expr -> expr
val __proj__Umod__item___1 : expr -> expr
val uu___is_MulMod : expr -> Prims.bool
val __proj__MulMod__item___0 : expr -> expr
val __proj__MulMod__item___1 : expr -> expr
val uu___is_NatToBv : expr -> Prims.bool
val __proj__NatToBv__item___0 : expr -> expr
type connective =
  1. | C_Lt
  2. | C_Eq
  3. | C_Gt
  4. | C_Ne
val uu___is_C_Lt : connective -> Prims.bool
val uu___is_C_Eq : connective -> Prims.bool
val uu___is_C_Gt : connective -> Prims.bool
val uu___is_C_Ne : connective -> Prims.bool
type prop =
  1. | CompProp of expr * connective * expr
  2. | AndProp of prop * prop
  3. | OrProp of prop * prop
  4. | NotProp of prop
val uu___is_CompProp : prop -> Prims.bool
val __proj__CompProp__item___0 : prop -> expr
val __proj__CompProp__item___1 : prop -> connective
val __proj__CompProp__item___2 : prop -> expr
val uu___is_AndProp : prop -> Prims.bool
val __proj__AndProp__item___0 : prop -> prop
val __proj__AndProp__item___1 : prop -> prop
val uu___is_OrProp : prop -> Prims.bool
val __proj__OrProp__item___0 : prop -> prop
val __proj__OrProp__item___1 : prop -> prop
val uu___is_NotProp : prop -> Prims.bool
val __proj__NotProp__item___0 : prop -> prop
val lt : expr -> expr -> prop
val le : expr -> expr -> prop
val eq : expr -> expr -> prop
val ne : expr -> expr -> prop
val gt : expr -> expr -> prop
val ge : expr -> expr -> prop
val return : 'a -> 'a tm
val bind : 'a tm -> ('a -> 'b tm) -> 'b tm
val liftM : ('a -> 'b) -> 'a tm -> 'b tm
val liftM2 : ('a -> 'b -> 'c) -> 'a tm -> 'b tm -> 'c tm
val liftM3 : ('a -> 'b -> 'c -> 'd) -> 'a tm -> 'b tm -> 'c tm -> 'd tm
val find_idx : ('a -> Prims.bool) -> 'a Prims.list -> (Prims.nat * 'a) FStar_Pervasives_Native.option
val fail : Prims.string -> 'a tm
type (!'a, 'p) refined_list_t = 'a Prims.list
val list_unref : 'a Prims.list -> 'a Prims.list
val as_arith_expr : FStar_Reflection_Types.term -> expr tm
val is_arith_expr : FStar_Reflection_Types.term -> expr tm
val is_arith_prop : FStar_Reflection_Types.term -> prop tm
val expr_to_string : expr -> Prims.string
val compare_expr : expr -> expr -> FStar_Order.order