gistfile1.txt

--------------------------------------------------------------------------------
--
-- List

struct nil:  List
struct cons: Z -> List -> List

head: List      -> V
    ( nil()     )= error
    ( cons(x _) )= x

    ( cons(3 nil) ) ? 3

tail: List       -> V
    ( nil()      )= error
    ( cons(_ xs) )= xs

    ( cons(3 nil) ) ? nil

length: List -> Z
      ( nil()      )= 0
      ( cons(_ xs) )= 1 + length(xs)

      ( nil )         ? 0
      ( cons(1 nil) ) ? 1

get: Z -> List      -> Z
   ( 0    cons(x _) )= x
   ( n    cons(_ x) )= get(n - 1 x)

reverse: List       -> List
       ( nil()      )= nil
       ( cons(x xs) )= concat(reverse(xs) cons(x nil))

       ( cons(1 nil) )         ? cons(1 nil)
       ( cons(1 cons(2 nil)) ) ? cons(2 cons(1 nil))

concat: List    -> List -> List
      ( nil()      x    )= x
      ( cons(x xs) y    )= cons(x concat(xs y))

      ( cons(1 nil) cons(2 nil) ) ? cons(1 cons(2 nil))

map: (Z -> Z) -> List       -> List
   ( f           nil()      )= nil
   ( f           cons(x xs) )= cons(f(x) map(f xs))

   ( fib cons(6 nil) ) ? cons(13 nil)

any: (Z -> B) -> List       -> B
   ( _           nil()      )= false
   ( f           cons(x xs) )= f(x) | any(f xs)



--------------------------------------------------------------------------------
--
-- Math

fib: Z -> Z
   ( 0 )= 1
   ( 1 )= 1
   ( n )= fib(n - 1) + fib(n - 2)

   (6) ? 13     
   (7) ? 21