ffalse ttrue in util.ml

src/transform/inlining.ml

@@ -17,14 +17,12 @@
 (*                                                                        *)
 (**************************************************************************)
 
+open Util
 open Ident
 open Term
 open Decl
 open Task
 
-let ttrue _ = true
-let ffalse _ = false
-
 type env = { fs : (vsymbol list * term) Mls.t;
              ps : (vsymbol list * fmla) Mls.t}
 

src/util/util.ml

@@ -58,6 +58,10 @@ exception FoldSkip
 let all_fn pr _ t = pr t || raise FoldSkip
 let any_fn pr _ t = pr t && raise FoldSkip
 
+(* constant boolean function *)
+let ttrue _ = true
+let ffalse _ = false
+
 (* Set and Map on strings *)
 
 module Sstr = Set.Make(String)

src/util/util.mli

@@ -47,6 +47,11 @@ exception FoldSkip
 val all_fn : ('a -> bool) -> 'b -> 'a -> bool
 val any_fn : ('a -> bool) -> 'b -> 'a -> bool
 
+val ffalse : 'a -> bool
+(** [ffalse] constant function [false] *)
+val ttrue : 'a -> bool
+(** [ttrue] constant function [true] *)
+
 (* Set and Map on strings *)
 
 module Sstr : Set.S with type elt = string