package alba

  1. Overview
  2. Docs

Module Alba_core.Sort

type t =
  1. | Proposition
  2. | Any of int
val compare : t -> t -> int

compare for sorting purposes.

val is_sub : t -> t -> bool

is_sub s1 s2 Is s1 a subtype of s2 (or equal)?

val is_super : t -> t -> bool

is_super s1 s2 Is s1 a supertype of s2 (or equal)?

val type_of : t -> t
val pi_sort : t -> t -> t

pi_sort sA sB computes the sort of a product term

    all (x: A): B

where A has sort sA and B has sort sB.