package dolmen

  1. Overview
  2. Docs
Module type
Class type

Minium required signature for tags to typecheck smtlib's core/base theory.

type term

The type of terms

type 'a t

Polymorphic tags

val named : string t

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

val triggers : term list t

Multi-triggers (typically annotated on the body of a quantified formula and not the quantified formula itself). Each term is a multi-trigger represented as a conjunction of triggers.

val rwrt : unit t

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