]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/common/level.mli
- new attributes system
[helm.git] / helm / software / helena / src / common / level.mli
index 9b4955248726eaffd5689491ee31e6af2af79227..4bae584fa8843ead6401d1d4260b9e54a207ebad 100644 (file)
@@ -9,19 +9,23 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
+type status
+
 type level
 
+val initial_status: unit -> status
+
 val infinite: level
 
 val finite: int -> level
 
-val is_zero: level -> bool
+val one: level
 
-val is_infinite: level -> bool
+val two: level
 
-val succ: level -> level
+val unknown: status -> Marks.mark -> level
 
-val pred: level -> level
+val is_zero: level -> bool
 
 val minus: level -> int -> level