fstar
  1. Overview
  2. Docs
package fstar
Legend:
Library
Module
Module type
Parameter
Class
Class type
type ('m, 'u, 'mult) right_unitality_lemma = Prims.unit
type ('m, 'u, 'mult) left_unitality_lemma = Prims.unit
type ('m, 'mult) associativity_lemma = Prims.unit
type !'m monoid =
  1. | Monoid of 'm * 'm -> 'm -> 'm * Prims.unit * Prims.unit * Prims.unit
val uu___is_Monoid : 'm monoid -> Prims.bool
val __proj__Monoid__item__unit : 'm monoid -> 'm
val __proj__Monoid__item__mult : 'm monoid -> 'm -> 'm -> 'm
val intro_monoid : 'm -> ('m -> 'm -> 'm) -> 'm monoid
val nat_plus_monoid : Prims.nat monoid
val int_plus_monoid : Prims.int monoid
val conjunction_monoid : Prims.unit monoid
val disjunction_monoid : Prims.unit monoid
val bool_and_monoid : Prims.bool monoid
val bool_or_monoid : Prims.bool monoid
val bool_xor_monoid : Prims.bool monoid
val lift_monoid_option : 'a monoid -> 'a FStar_Pervasives_Native.option monoid
type ('a, 'b, 'f, 'ma, 'mb) monoid_morphism_unit_lemma = Prims.unit
type ('a, 'b, 'f, 'ma, 'mb) monoid_morphism_mult_lemma = Prims.unit
type (!'a, !'b, !'f, !'ma, !'mb) monoid_morphism =
  1. | MonoidMorphism of Prims.unit * Prims.unit
val uu___is_MonoidMorphism : ('a -> 'b) -> 'a monoid -> 'b monoid -> ('a, 'b, Prims.unit, Prims.unit, Prims.unit) monoid_morphism -> Prims.bool
val intro_monoid_morphism : ('a -> 'b) -> 'a monoid -> 'b monoid -> ('a, 'b, Prims.unit, Prims.unit, Prims.unit) monoid_morphism
val embed_nat_int : Prims.nat -> Prims.int
val uu___154 : (Prims.nat, Prims.int, Prims.unit, Prims.unit, Prims.unit) monoid_morphism
type 'p neg = Prims.unit
val uu___156 : (Prims.unit, Prims.unit, Prims.unit neg, Prims.unit, Prims.unit) monoid_morphism
val uu___165 : (Prims.unit, Prims.unit, Prims.unit neg, Prims.unit, Prims.unit) monoid_morphism
type ('m, 'a, 'mult, 'act) mult_act_lemma = Prims.unit
type ('m, 'a, 'u, 'act) unit_act_lemma = Prims.unit
type (!'m, !'mm, !'a) left_action =
  1. | LAct of 'm -> 'a -> 'a * Prims.unit * Prims.unit
val uu___is_LAct : 'm monoid -> Prims.unit -> ('m, Prims.unit, Obj.t) left_action -> Prims.bool
val __proj__LAct__item__act : 'm monoid -> Prims.unit -> ('m, Prims.unit, Obj.t) left_action -> 'm -> Obj.t -> Obj.t
type ('a, 'b, 'ma, 'mb, 'f, 'mf, 'mma, 'mmb, 'la, 'lb) left_action_morphism = Prims.unit