CLogic.CFormula
type t =
| True
| False
| Eq of CExpr.t * CExpr.t
| Less of CExpr.t * CExpr.t
| LessEq of CExpr.t * CExpr.t
| SetMem of CExpr.t * CExpr.t
| And of t * t
| Or of t * t
| Not of t
| Implies of t * t
| ForAll of (string * GilType.t option) list * t
val pp : Stdlib.Format.formatter -> t -> unit