functor (C : sig type t val context : Syntax.Infix.t Syntax.context end) ->
  sig
    val exists :
      ?name:string ->
      Syntax.typ_fo -> C.t Syntax.formula -> C.t Syntax.formula
    val forall :
      ?name:string ->
      Syntax.typ_fo -> C.t Syntax.formula -> C.t Syntax.formula
    val ( ! ) : C.t Syntax.formula -> C.t Syntax.formula
    val ( && ) :
      C.t Syntax.formula -> C.t Syntax.formula -> C.t Syntax.formula
    val ( || ) :
      C.t Syntax.formula -> C.t Syntax.formula -> C.t Syntax.formula
    val ( < ) : C.t Syntax.term -> C.t Syntax.term -> C.t Syntax.formula
    val ( <= ) : C.t Syntax.term -> C.t Syntax.term -> C.t Syntax.formula
    val ( = ) : C.t Syntax.term -> C.t Syntax.term -> C.t Syntax.formula
    val tru : C.t Syntax.formula
    val fls : C.t Syntax.formula
    val ( + ) : C.t Syntax.term -> C.t Syntax.term -> C.t Syntax.term
    val ( - ) : C.t Syntax.term -> C.t Syntax.term -> C.t Syntax.term
    val ( * ) : C.t Syntax.term -> C.t Syntax.term -> C.t Syntax.term
    val ( / ) : C.t Syntax.term -> C.t Syntax.term -> C.t Syntax.term
    val ( mod ) : C.t Syntax.term -> C.t Syntax.term -> C.t Syntax.term
    val const : Syntax.symbol -> (C.t, 'typ) Syntax.expr
    val var : int -> Syntax.typ_fo -> (C.t, 'typ) Syntax.expr
  end