Module Osiris.Coq

type expression =
  1. | CAtom of string
  2. | CCon of string * expression list
  3. | CList of expression list
  4. | CTuple of expression list
  5. | CCut of string * expression

A highly minimalistic abstract syntax of Coq expressions.

type def = {
  1. lhs : string;
  2. rhs : expression;
}

Coq toplevel definitions.

type defs = def list
val plain : string -> expression
val c : string -> expression list -> expression
val list : expression list -> expression
val clist : string -> expression list -> expression
val tuple : expression list -> expression
val cut : string -> expression -> expression