[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

reduce_nat( ... )



Hi to everybody,

    who knows where can I find the definition of the function 
 reduce_nat(....).
It is used in the prelude file in the list_props THEORY :


  length(l): RECURSIVE nat =
    CASES l OF
      null: 0,
      cons(x, y): length(y) + 1
    ENDCASES
   MEASURE reduce_nat(0, (LAMBDA (x: T), (n: nat): n + 1))


thanks,
Mauro.

-- 
---------------------------------------------------------------------------
  Mauro Gargano
  University of Saarland, Saarbruecken, DE
  Computer Architecture and Parallel Computing
  building 45, room 320                            mauro@wjp.cs.uni-sb.de
---------------------------------------------------------------------------