package dolmen

  1. Overview
  2. Docs
type t
type id
type term
type location
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