sig
  type t
  type id
  type term
  type location
  val data :
    ?loc:Ast_zf.Statement.location ->
    Ast_zf.Statement.t list -> Ast_zf.Statement.t
  val decl :
    ?loc:Ast_zf.Statement.location ->
    Ast_zf.Statement.id -> Ast_zf.Statement.term -> Ast_zf.Statement.t
  val definition :
    ?loc:Ast_zf.Statement.location ->
    Ast_zf.Statement.id ->
    Ast_zf.Statement.term -> Ast_zf.Statement.term -> Ast_zf.Statement.t
  val inductive :
    ?loc:Ast_zf.Statement.location ->
    Ast_zf.Statement.id ->
    Ast_zf.Statement.term list ->
    (Ast_zf.Statement.id * Ast_zf.Statement.term list) list ->
    Ast_zf.Statement.t
  val rewrite :
    ?loc:Ast_zf.Statement.location ->
    ?attr:Ast_zf.Statement.term ->
    Ast_zf.Statement.term -> Ast_zf.Statement.t
  val goal :
    ?loc:Ast_zf.Statement.location ->
    ?attr:Ast_zf.Statement.term ->
    Ast_zf.Statement.term -> Ast_zf.Statement.t
  val assume :
    ?loc:Ast_zf.Statement.location ->
    ?attr:Ast_zf.Statement.term ->
    Ast_zf.Statement.term -> Ast_zf.Statement.t
end