Commit a7930794 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

test functions is_ts_tuple...

parent 82adadd5
......@@ -521,6 +521,8 @@ let fs_tuple n =
let fs_tuple = Util.memo fs_tuple
let is_fs_tuple fs = fs == fs_tuple (List.length fs.ls_args)
let t_tuple tl =
let ty = ty_tuple (List.map (fun t -> t.t_ty) tl) in
t_app (fs_tuple (List.length tl)) tl ty
......
......@@ -288,6 +288,8 @@ val f_neq_simp : term -> term -> fmla
val fs_tuple : int -> lsymbol
val t_tuple : term list -> term
val is_fs_tuple : lsymbol -> bool
(** Term library *)
(* generic term/fmla traversal *)
......
......@@ -218,3 +218,4 @@ let ts_tuple = Util.memo ts_tuple
let ty_tuple tyl =
ty_app (ts_tuple (List.length tyl)) tyl
let is_ts_tuple ts = ts == ts_tuple (List.length ts.ts_args)
......@@ -97,3 +97,5 @@ val ty_real : ty
val ts_tuple : int -> tysymbol
val ty_tuple : ty list -> ty
val is_ts_tuple : tysymbol -> bool
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment