package dolmen

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

Module Expr.TagsSource

Sourcetype 'a t = 'a tag

Polymorphic tags

Sourceval 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
Sourceval rwrt : unit t

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

Sourcetype name

A type used to specify a name for printing identifiers

Sourceval name : name t

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

Sourceval exact : string -> name

Print the identifier with this exact string.

Sourcetype pos

A type to indicate how to print identifiers

Sourceval pos : pos t

A tag to specify how to print identifiers

Sourceval infix : pos

The tagged identifier is an infix symbol

Sourceval 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
Sourceval 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.

Sourceval named : string t

A tag used to name formulas in alt-ergo.

Sourceval triggers : term list list t

Multi-triggers that can be added to quantified formulas

Sourceval filters : term list t

Filters that can be added to quantified formulas