package dolmen

  1. Overview
  2. Docs
package dolmen
Legend:
Library
Module
Module type
Parameter
Class
Class type

Minium required signature for tags to typecheck Alt-Ergo's core/base theory.

type term

The type of terms

type 'a t

Polymorphic tags

val predicate : unit t

A flag (i.e. unit tag), indicating that the declaration is a predicate

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 : term list t

Multi-triggers that can be added to quantified formulas. Each term is a multi-trigger represented as a conjunction of triggers.

val filters : term list t

Filters that can be added to quantified formulas