fstar 2025.02.17 · OCaml Package

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 =

| 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 =

| 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___0 : 
  (Prims.nat, Prims.int, Prims.unit, Prims.unit, Prims.unit) monoid_morphism

type 'p neg = Prims.unit

val uu___1 : 
  (Prims.unit, Prims.unit, Prims.unit neg, Prims.unit, Prims.unit)
    monoid_morphism

val uu___2 : 
  (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 =

| 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

package fstar