-
-exception NotClosed
-
-let is_closed t =
- try
- let rec aux k _ = function
- | NCic.Rel n when n > k -> raise NotClosed
- | NCic.Meta (_, (s, NCic.Irl n)) when not (n+s <= k) -> raise NotClosed
- | NCic.Meta (_, (s, NCic.Ctx l)) -> List.iter (aux (k+s) ()) l
- | _ -> fold aux ((+) 1) () k t
- in
- aux 0 () t; true
- with NotClosed -> false
-;;
-