feat(core): improve Lit

src/core/Sidekick_core.ml

@@ -23,9 +23,11 @@ module Term = struct
   include Sidekick_core_logic.T_builtins
 end
 
-module Var = Sidekick_core_logic.Var
 module Bvar = Sidekick_core_logic.Bvar
-module Subst = Sidekick_core_logic.Subst
+module Lit = Lit
-module Proof_trace = Proof_trace
-module Proof_sat = Proof_sat
 module Proof_core = Proof_core
+module Proof_sat = Proof_sat
+module Proof_trace = Proof_trace
+module Proof_term = Proof_term
+module Subst = Sidekick_core_logic.Subst
+module Var = Sidekick_core_logic.Var

src/core/lit.ml

@@ -21,6 +21,10 @@ let atom ?(sign = true) (t : term) : t =
   in
   make ~sign t
 
+let make_eq ?sign store t u : t =
+  let p = T_builtins.eq store t u in
+  atom ?sign p
+
 let equal a b = a.lit_sign = b.lit_sign && T.equal a.lit_term b.lit_term
 
 let hash a =

src/core/lit.mli

@@ -36,6 +36,8 @@ val atom : ?sign:bool -> term -> t
       its sign in the process.
       @param sign if provided, and [sign=false], negate the resulting lit. *)
 
+val make_eq : ?sign:bool -> Term.store -> term -> term -> t
+
 val norm_sign : t -> t * bool
 (** [norm_sign (+t)] is [+t, true],
       and [norm_sign (-t)] is [+t, false].