diff options
author | ckeller <ckeller@users.noreply.github.com> | 2021-02-23 17:06:51 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-23 17:06:51 +0100 |
commit | 240b76807340e59bb85b35e3ebbb807792459912 (patch) | |
tree | 22d60d5c8db5034bdd9045e8579df14406ac69bc /src/trace/smtBtype.mli | |
parent | 74558c622de91801e3e188bdf690eb9a665f965b (diff) | |
download | smtcoq-240b76807340e59bb85b35e3ebbb807792459912.tar.gz smtcoq-240b76807340e59bb85b35e3ebbb807792459912.zip |
Link equality on uninterpreted sorts with SMT equality (#86)
Equality is now treated from uninterpreted sorts, which makes them usable with tactics!
Closes #17
Closes #78
Diffstat (limited to 'src/trace/smtBtype.mli')
-rw-r--r-- | src/trace/smtBtype.mli | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/src/trace/smtBtype.mli b/src/trace/smtBtype.mli index 5d45ca4..5710cf3 100644 --- a/src/trace/smtBtype.mli +++ b/src/trace/smtBtype.mli @@ -13,11 +13,11 @@ open SmtMisc -type indexed_type = Structures.constr gen_hashed +type indexed_type val dummy_indexed_type: int -> indexed_type val indexed_type_index : indexed_type -> int -val indexed_type_hval : indexed_type -> Structures.constr +val indexed_type_compdec : indexed_type -> Structures.constr type btype = | TZ @@ -27,9 +27,9 @@ type btype = | TFArray of btype * btype | Tindex of indexed_type -val indexed_type_of_int : int -> Structures.constr SmtMisc.gen_hashed +val indexed_type_of_int : int -> indexed_type -val equal : btype -> btype -> bool +module HashedBtype : Hashtbl.HashedType with type t = btype val to_coq : btype -> Structures.constr @@ -39,9 +39,8 @@ type reify_tbl val create : unit -> reify_tbl -val declare : reify_tbl -> Structures.constr -> Structures.constr -> btype - val of_coq : reify_tbl -> logic -> Structures.constr -> btype +val of_coq_compdec : reify_tbl -> Structures.constr -> Structures.constr -> btype val get_coq_type_op : int -> Structures.constr |