Module type Zf.Statement

module type Statement = Ast_zf.Statement

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 data : ?loc:location ->
       t list -> t

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

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

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

val rewrite : ?loc:location ->
       ?attr:term -> term -> t

val goal : ?loc:location ->
       ?attr:term -> term -> t

val assume : ?loc:location ->
       ?attr:term -> term -> t