A (sidekick.Sidekick_smt_solver.Make.1-A)

module T : Sidekick_core.TERM

module Lit : Sidekick_core.LIT with module T = T

type proof

type proof_step

module P : Sidekick_core.PROOF with type term = T.Term.t and type t = proof and type proof_step = proof_step and type lit = Lit.t

val cc_view : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) Sidekick_core.CC_view.t

val is_valid_literal : T.Term.t -> bool

Is this a valid boolean literal? (e.g. is it a closed term, not inside a quantifier)