fstar
  1. Overview
  2. Docs
package fstar
Legend:
Library
Module
Module type
Parameter
Class
Class type
type ('a, 'cmuadd, 'cmumult) distribute_left_lemma = Prims.unit
type ('a, 'cmuadd, 'cmumult) distribute_right_lemma = Prims.unit
type ('a, 'cmuadd, 'cmumult) mult_zero_l_lemma = Prims.unit
type ('a, 'cmuadd, 'opp) add_opp_r_lemma = Prims.unit
val uu___is_CR : 'a cr -> Prims.bool
val __proj__CR__item__cm_add : 'a cr -> 'a FStar_Algebra_CommMonoid.cm
val __proj__CR__item__cm_mult : 'a cr -> 'a FStar_Algebra_CommMonoid.cm
val __proj__CR__item__opp : 'a cr -> 'a -> 'a
val norm_fully : 'a -> 'a
type index = Prims.nat
type varlist =
  1. | Nil_var
  2. | Cons_var of index * varlist
val uu___is_Nil_var : varlist -> Prims.bool
val uu___is_Cons_var : varlist -> Prims.bool
val __proj__Cons_var__item___0 : varlist -> index
val __proj__Cons_var__item___1 : varlist -> varlist
type !'a canonical_sum =
  1. | Nil_monom
  2. | Cons_monom of 'a * varlist * 'a canonical_sum
  3. | Cons_varlist of varlist * 'a canonical_sum
val uu___is_Nil_monom : 'a canonical_sum -> Prims.bool
val uu___is_Cons_monom : 'a canonical_sum -> Prims.bool
val __proj__Cons_monom__item___0 : 'a canonical_sum -> 'a
val __proj__Cons_monom__item___1 : 'a canonical_sum -> varlist
val __proj__Cons_monom__item___2 : 'a canonical_sum -> 'a canonical_sum
val uu___is_Cons_varlist : 'a canonical_sum -> Prims.bool
val __proj__Cons_varlist__item___0 : 'a canonical_sum -> varlist
val __proj__Cons_varlist__item___1 : 'a canonical_sum -> 'a canonical_sum
val varlist_lt : varlist -> varlist -> Prims.bool
val varlist_merge : varlist -> varlist -> varlist
val vm_aux : index -> varlist -> varlist -> varlist
val canonical_sum_merge : 'a cr -> 'a canonical_sum -> 'a canonical_sum -> 'a canonical_sum
val csm_aux : 'a cr -> 'a -> varlist -> 'a canonical_sum -> 'a canonical_sum -> 'a canonical_sum
val monom_insert : 'a cr -> 'a -> varlist -> 'a canonical_sum -> 'a canonical_sum
val varlist_insert : 'a cr -> varlist -> 'a canonical_sum -> 'a canonical_sum
val canonical_sum_scalar : 'a cr -> 'a -> 'a canonical_sum -> 'a canonical_sum
val canonical_sum_scalar2 : 'a cr -> varlist -> 'a canonical_sum -> 'a canonical_sum
val canonical_sum_scalar3 : 'a cr -> 'a -> varlist -> 'a canonical_sum -> 'a canonical_sum
val canonical_sum_prod : 'a cr -> 'a canonical_sum -> 'a canonical_sum -> 'a canonical_sum
type !'a spolynomial =
  1. | SPvar of index
  2. | SPconst of 'a
  3. | SPplus of 'a spolynomial * 'a spolynomial
  4. | SPmult of 'a spolynomial * 'a spolynomial
val uu___is_SPvar : 'a spolynomial -> Prims.bool
val __proj__SPvar__item___0 : 'a spolynomial -> index
val uu___is_SPconst : 'a spolynomial -> Prims.bool
val __proj__SPconst__item___0 : 'a spolynomial -> 'a
val uu___is_SPplus : 'a spolynomial -> Prims.bool
val __proj__SPplus__item___0 : 'a spolynomial -> 'a spolynomial
val __proj__SPplus__item___1 : 'a spolynomial -> 'a spolynomial
val uu___is_SPmult : 'a spolynomial -> Prims.bool
val __proj__SPmult__item___0 : 'a spolynomial -> 'a spolynomial
val __proj__SPmult__item___1 : 'a spolynomial -> 'a spolynomial
val spolynomial_normalize : 'a cr -> 'a spolynomial -> 'a canonical_sum
val canonical_sum_simplify : 'a cr -> 'a canonical_sum -> 'a canonical_sum
val spolynomial_simplify : 'a cr -> 'a spolynomial -> 'a canonical_sum
type !'a vmap = (FStar_Reflection_Data.var * 'a) Prims.list * 'a
val update : FStar_Reflection_Data.var -> 'a -> 'a vmap -> 'a vmap
val interp_var : 'a vmap -> index -> 'a
val ivl_aux : 'a cr -> 'a vmap -> index -> varlist -> 'a
val interp_vl : 'a cr -> 'a vmap -> varlist -> 'a
val interp_m : 'a cr -> 'a vmap -> 'a -> varlist -> 'a
val ics_aux : 'a cr -> 'a vmap -> 'a -> 'a canonical_sum -> 'a
val interp_cs : 'a cr -> 'a vmap -> 'a canonical_sum -> 'a
val interp_sp : 'a cr -> 'a vmap -> 'a spolynomial -> 'a
type !'a polynomial =
  1. | Pvar of index
  2. | Pconst of 'a
  3. | Pplus of 'a polynomial * 'a polynomial
  4. | Pmult of 'a polynomial * 'a polynomial
  5. | Popp of 'a polynomial
val uu___is_Pvar : 'a polynomial -> Prims.bool
val __proj__Pvar__item___0 : 'a polynomial -> index
val uu___is_Pconst : 'a polynomial -> Prims.bool
val __proj__Pconst__item___0 : 'a polynomial -> 'a
val uu___is_Pplus : 'a polynomial -> Prims.bool
val __proj__Pplus__item___0 : 'a polynomial -> 'a polynomial
val __proj__Pplus__item___1 : 'a polynomial -> 'a polynomial
val uu___is_Pmult : 'a polynomial -> Prims.bool
val __proj__Pmult__item___0 : 'a polynomial -> 'a polynomial
val __proj__Pmult__item___1 : 'a polynomial -> 'a polynomial
val uu___is_Popp : 'a polynomial -> Prims.bool
val __proj__Popp__item___0 : 'a polynomial -> 'a polynomial
val polynomial_normalize : 'a cr -> 'a polynomial -> 'a canonical_sum
val polynomial_simplify : 'a cr -> 'a polynomial -> 'a canonical_sum
val spolynomial_of : 'a cr -> 'a polynomial -> 'a spolynomial
val interp_p : 'a cr -> 'a vmap -> 'a polynomial -> 'a
val int_cr : Prims.int cr