EAFormula.mli

(* This module implements formulas with global box and global diamond (A, E) *)

module CA = CoAlgFormula

type eaformula =
  | TRUE
  | FALSE
  | AP of string (*named atom*)
  | NOT of eaformula
  | OR of eaformula * eaformula
  | AND of eaformula * eaformula
  | EQU of eaformula * eaformula
  | IMP of eaformula * eaformula
  | EX of string * eaformula (* exists, diamond of K *)
  | AX of string * eaformula (* forall, box of K *)
  | ID of eaformula (* modality of the identity functor *)
  | E_AP of string (* global diamond *)
  | A of eaformula (* global box *)

val exportFormula : eaformula -> string
val nom2EA : CoAlgFormula.formula -> eaformula

(* vim: set et sw=2 sts=2 ts=8 : *)