diff --git a/src/base/Uconst.ml b/src/base/Uconst.ml index 37478704..7f879b07 100644 --- a/src/base/Uconst.ml +++ b/src/base/Uconst.ml @@ -60,6 +60,11 @@ let uconst_of_id' tst id args ret = let uconst_of_str tst name args ret : term = uconst_of_id' tst (ID.make name) args ret +let is_uconst (t : Term.t) = + match Term.view t with + | Term.E_const { Const.c_view = Uconst _; _ } -> true + | _ -> false + module As_key = struct type nonrec t = t diff --git a/src/base/Uconst.mli b/src/base/Uconst.mli index d069e4c4..7b983c2b 100644 --- a/src/base/Uconst.mli +++ b/src/base/Uconst.mli @@ -21,6 +21,7 @@ val uconst : Term.store -> t -> Term.t val uconst_of_id : Term.store -> ID.t -> ty -> Term.t val uconst_of_id' : Term.store -> ID.t -> ty list -> ty -> Term.t val uconst_of_str : Term.store -> string -> ty list -> ty -> Term.t +val is_uconst : Term.t -> bool module Map : CCMap.S with type key = t module Tbl : CCHashtbl.S with type key = t