fstar
  1. Overview
  2. Docs
package fstar
Legend:
Library
Module
Module type
Parameter
Class
Class type
type atom = Prims.nat
type exp =
  1. | Unit
  2. | Mult of exp * exp
  3. | Atom of atom
val uu___is_Unit : exp -> Prims.bool
val uu___is_Mult : exp -> Prims.bool
val __proj__Mult__item___0 : exp -> exp
val __proj__Mult__item___1 : exp -> exp
val uu___is_Atom : exp -> Prims.bool
val __proj__Atom__item___0 : exp -> atom
val exp_to_string : exp -> Prims.string
type !'a amap = (atom * 'a) Prims.list * 'a
val const : 'a -> 'a amap
val select : atom -> 'a amap -> 'a
val update : atom -> 'a -> 'a amap -> 'a amap
val mdenote : 'a FStar_Algebra_CommMonoid.cm -> 'a amap -> exp -> 'a
val xsdenote : 'a FStar_Algebra_CommMonoid.cm -> 'a amap -> atom Prims.list -> 'a
val flatten : exp -> atom Prims.list
type permute = atom Prims.list -> atom Prims.list
type 'p permute_correct = Prims.unit
type 'p permute_via_swaps = Prims.unit
val sort : permute
val canon : exp -> atom Prims.list