package dolmen

  1. Overview
  2. Docs
package dolmen
Legend:
Library
Module
Module type
Parameter
Class
Class type
type 'a t = 'a tag

Polymorphic tags

val bound : term tag

Tag used one let-bound variables to reference the defining term for the variable (i.e. the term to which it is let-bound).

Satsify the Smtlib interface.

include Dolmen_intf.Tag.Smtlib_Base with type 'a t := 'a t and type term := term

Satsify the Zf interface.

include Dolmen_intf.Tag.Zf_Base with type 'a t := 'a t and type pos = Pretty.pos
val rwrt : unit t

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

type name

A type used to specify a name for printing identifiers

val name : name t

A tag used to specify what to print when printing an identifier

val exact : string -> name

Print the identifier with this exact string.

type pos = Pretty.pos

A type to indicate how to print identifiers

val pos : pos t

A tag to specify how to print identifiers

val infix : pos

The tagged identifier is an infix symbol

val prefix : pos

The tagged identifier is a prefix symbol

Satsify the Ae interface.

include Dolmen_intf.Tag.Ae_Base with type 'a t := 'a t and type term := term
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