From 91d5c0fa85b3feaf92d3978bbb673f7944c7d2ff Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 1 Nov 2022 22:22:06 -0400 Subject: [PATCH] detail in sidekick_base --- src/base/Uconst.ml | 5 +++++ src/base/Uconst.mli | 1 + 2 files changed, 6 insertions(+) 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