fstar
  1. Overview
  2. Docs
package fstar
Legend:
Library
Module
Module type
Parameter
Class
Class type
type atom = Prims.int
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 flatten : exp -> atom Prims.list
type permute = atom Prims.list -> atom Prims.list
type 'p permute_correct = Prims.unit
type 'n swap = Prims.nat
val apply_swap_aux : Prims.nat -> 'a Prims.list -> Prims.nat -> 'a Prims.list
val apply_swap : Prims.unit -> 'a Prims.list -> Prims.nat -> 'a Prims.list
val apply_swaps : 'a Prims.list -> Prims.nat Prims.list -> 'a Prims.list
type 'p permute_via_swaps = Prims.unit
val sort : permute
val canon : exp -> atom Prims.list
val quote_exp : exp -> FStar_Reflection_Types.term