package dolmen

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

Implementation requirements for the Zipperposition format.

type t

The type of statements.

type id

The type of identifiers

type term

The type of terms used in statements.

type location

The type of locations attached to statements.

val import : ?loc:location -> string -> t

val data : ?loc:location -> ?attrs:term list -> t list -> t

val defs : ?loc:location -> ?attrs:term list -> t list -> t

val rewrite : ?loc:location -> ?attrs:term list -> term -> t

val goal : ?loc:location -> ?attrs:term list -> term -> t

val assume : ?loc:location -> ?attrs:term list -> term -> t

val lemma : ?loc:location -> ?attrs:term list -> term -> t

val decl : ?loc:location -> ?attrs:term list -> id -> term -> t

val definition : 
  ?loc:location ->
  ?attrs:term list ->
  id ->
  term ->
  term list ->
  t

val inductive : 
  ?loc:location ->
  ?attrs:term list ->
  id ->
  term list ->
  (id * term list) list ->
  t