fstar
  1. Overview
  2. Docs
package fstar
Legend:
Library
Module
Module type
Parameter
Class
Class type
type (!'Ap1, !'Ap2) cand =
  1. | Conj of 'Ap1 * 'Ap2
val uu___is_Conj : 'a -> bool
val __proj__Conj__item__h1 : ('a, 'b) cand -> 'a
val __proj__Conj__item__h2 : ('a, 'b) cand -> 'b
type (!'Ap1, !'Ap2) cor =
  1. | IntroL of 'Ap1
  2. | IntroR of 'Ap2
val uu___is_IntroL : ('a, 'b) cor -> bool
val __proj__IntroL__item__h : ('a, 'b) cor -> 'a
val uu___is_IntroR : ('a, 'b) cor -> bool
val __proj__IntroR__item__h : ('a, 'b) cor -> 'b
type (!'Aa, !'Ab) cimp = 'Aa -> 'Ab
type (!'Aa, !'Ab) ciff = (('Aa, 'Ab) cimp, ('Ab, 'Aa) cimp) cand
type (!'Aa, !'Ap) cexists =
  1. | ExIntro of 'Aa * 'Ap
val uu___is_ExIntro : 'a -> bool
val __proj__ExIntro__item__x : ('a, 'b) cexists -> 'a
val __proj__ExIntro__item__h : ('a, 'b) cexists -> 'b
type (!'Aa, !'Ax, !'dummyV0) ceq =
  1. | Refl
val uu___is_Refl : 'a -> 'b -> 'c -> bool
type (!'Aa, !'dummyV0) ceq_type =
  1. | ReflType
val uu___is_ReflType : 'a -> bool
val eq_ind : 'a -> 'b -> 'c -> 'd -> 'e -> 'c
val ceq_eq : 'a -> 'b -> 'c -> unit
val ceq_congruence : 'a -> 'b -> 'c -> 'd -> 'e
val ceq_symm : 'a -> 'b -> 'c -> ('d, 'e, 'f) ceq
val ceq_trans : 'a -> 'b -> 'c -> 'd -> 'e -> ('f, 'g, 'h) ceq
type ctrue =
  1. | I
val uu___is_I : ctrue -> Prims.bool
type cfalse
val cfalse_elim : 'a
val false_elim2 : 'a -> 'b
val false_elim : 'a -> 'b
type !'Ap cnot = ('Ap, cfalse) cimp