package tyabt

  1. Overview
  2. Docs
type 'sort t

A variable annotated by its sort.

type 'sort sort = 'sort Sort.t

A sort.

val fresh : 'sort sort -> string -> 'sort t

Generates a fresh variable of the given sort. The variable is unique from any other variable generated from the function.

val sort : 'sort t -> 'sort sort

Retrieves the sort of the variable.

val name : _ t -> string

Retrieves the name of the variable.

val equal : 'sort1 t -> 'sort2 t -> ('sort1, 'sort2) eq option

Checks two variables for equality. Iff the variables are equal, returns Some proof that their sorts are the same.