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
Sourceval named : string t

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

Sourceval triggers : term list t

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

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