module type Term = Ast_zf.Term
type
The type of terms.
type
The type of identifiers
type
The type of locations attached to terms.
val tType : t
val wildcard : t
val prop : t
val true_ : t
val false_ : t
Standard pre-defined constants.
val const : ?loc:location -> id -> t
Create a new constant.
val apply : ?loc:location ->
t -> t list -> t
Application of terms.
val colon : ?loc:location -> t -> t -> t
Juxtaposition of terms, usually used for annotating terms with types.
val arrow : ?loc:location -> t -> t -> t
Arow, i.e function type constructor, currifyed.
val eq : ?loc:location -> t -> t -> t
Make an equality between terms.
val not_ : ?loc:location -> t -> t
val or_ : ?loc:location -> t list -> t
val and_ : ?loc:location -> t list -> t
val imply : ?loc:location -> t -> t -> t
val equiv : ?loc:location -> t -> t -> t
Usual propositional functions.
val pi : ?loc:location ->
t list -> t -> t
Dependant product, or polymorphic type quantification.
Used to build polymorphic function types such as,
Pi [a] (Arrow a a).
val letin : ?loc:location ->
t list -> t -> t
Local term binding.
val forall : ?loc:location ->
t list -> t -> t
Universal propositional quantification.
val exists : ?loc:location ->
t list -> t -> t
Existencial porpositional qantification.