src/Pure/pattern.ML
changeset 23222 daca4731942f
parent 22678 23963361278c
child 25473 812db0f215b3
     1.1 --- a/src/Pure/pattern.ML	Sun Jun 03 23:16:49 2007 +0200
     1.2 +++ b/src/Pure/pattern.ML	Sun Jun 03 23:16:50 2007 +0200
     1.3 @@ -151,7 +151,11 @@
     1.4    in Envir.update (((F, T), mkhnf (binders, is, G, js)), env') end;
     1.5  
     1.6  
     1.7 -(* mk_proj_list(is) = [ |is| - k | 1 <= k <= |is| and is[k] >= 0 ] *)
     1.8 +(*predicate: downto0 (is, n) <=> is = [n, n - 1, ..., 0]*)
     1.9 +fun downto0 (i :: is, n) = i = n andalso downto0 (is, n - 1)
    1.10 +  | downto0 ([], n) = n = ~1;
    1.11 +
    1.12 +(*mk_proj_list(is) = [ |is| - k | 1 <= k <= |is| and is[k] >= 0 ]*)
    1.13  fun mk_proj_list is =
    1.14      let fun mk(i::is,j) = if is_some i then j :: mk(is,j-1) else mk(is,j-1)
    1.15            | mk([],_)    = []