dolmen_type

A typechecker for automated deduction languages
IN THIS PACKAGE
Parameter #2 Dolmen_type . Core . Ae . Tff . Tag
type 'a t = 'a Type.Tag.t

Polymorphic tags

val ac : unit t

A flag (i.e. unit tag), indicating that the tagged term/formula is to be considered as a associative and commutative term.

val named : string t

A tag used to name formulas in alt-ergo.

val triggers : Type.T.t list list t

Multi-triggers that can be added to quantified formulas

val filters : Type.T.t list t

Filters that can be added to quantified formulas