From a8f2c7ca6806a563808eba60fadd2e1dbaec49e4 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 14 Apr 2004 13:56:47 +0000 Subject: [PATCH] added exists_meta --- helm/ocaml/cic/cicUtil.ml | 2 ++ helm/ocaml/cic/cicUtil.mli | 3 +++ 2 files changed, 5 insertions(+) diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml index fb40ad3ba..55a70822e 100644 --- a/helm/ocaml/cic/cicUtil.ml +++ b/helm/ocaml/cic/cicUtil.ml @@ -30,6 +30,8 @@ let lookup_meta index metasenv = List.find (fun (index', _, _) -> index = index') metasenv with Not_found -> raise (Meta_not_found index) +let exists_meta index = List.exists (fun (index', _, _) -> (index = index')) + let is_closed = let module C = Cic in let rec is_closed k = diff --git a/helm/ocaml/cic/cicUtil.mli b/helm/ocaml/cic/cicUtil.mli index 7db463b7d..9069c24fb 100644 --- a/helm/ocaml/cic/cicUtil.mli +++ b/helm/ocaml/cic/cicUtil.mli @@ -22,8 +22,11 @@ * For details, see the HELM World-Wide-Web page, * http://helm.cs.unibo.it/ *) + exception Meta_not_found of int val lookup_meta: int -> Cic.metasenv -> Cic.conjecture +val exists_meta: int -> Cic.metasenv -> bool val is_closed : Cic.term -> bool + -- 2.39.2