dolmen_type

A typechecker for automated deduction languages
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library dolmen_type
Parameter #2 Dolmen_type . Core . Smtlib2 . Tff . Tag
type 'a t = 'a Type.Tag.t

Polymorphic tags

val named : string t

A tag used to named formulas in smtlib. Should correspond to the `:named` attribute.

val triggers : Type.T.t list list t

Multi-triggers (typically annotated on the body of a quantified formula and not the quantified formula itself).

val rwrt : unit t

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