simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 03:05:31 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

detail in sidekick_base

Browse source
This commit is contained in:
Simon Cruanes 2022-11-01 22:22:06 -04:00
parent 5a7ca4ca2e
commit 91d5c0fa85
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
2 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/base/Uconst.ml
View file

@ -60,6 +60,11 @@ let uconst_of_id' tst id args ret =
let uconst_of_str tst name args ret : term = let uconst_of_str tst name args ret : term =
uconst_of_id' tst (ID.make name) args ret 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 module As_key = struct
type nonrec t = t type nonrec t = t

1
src/base/Uconst.mli
View file

@ -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 -> Term.t
val uconst_of_id' : Term.store -> ID.t -> ty list -> 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 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 Map : CCMap.S with type key = t
module Tbl : CCHashtbl.S with type key = t module Tbl : CCHashtbl.S with type key = t