Text/ParserCombinators/Parsec/examples/Henk/test.h

   1 -- type declarations
   2 data List: * -> *
   3     = { Nil: \/a. List a
   4           ; Cons : \/a. a -> List a -> List a
   5           };
   6
   7 data Maybe : * -> * -> *
   8         = { Left:  \/a,b. a -> Maybe a b
   9       ; Right:  \/a,b. b -> Maybe a b
  10       }
  11
  12 -- value declarations
  13 let id : \/a. a->a
  14         = /\a. \x:a. x;
  15
  16 letrec { map: \/a,b. a -> b -> List a -> List b
  17         = /\a,b.
  18       \f: a->b,xs:List a.
  19               case (xs) of
  20               { Nil =>Nil
  21               ; Cons => \x:a, xx: List a.
  22                                         Cons (f x) (map a b f xx)
  23               }
  24               at {a:*}
  25           };
  26
  27 letrec { reverse: \/a. List a -> List a
  28               = /\a.\xs:List a.
  29                  case xs of
  30                  { Nil => Nil
  31                  ; Cons x,xx => append (reverse xx) (Cons x Nil)
  32                  }
  33                  at {a:*}
  34            };
  35
  36 letrec { append: \/a. |~|_dummy:List a.|~|_:List a.List a
  37            = /\a.\xs:List a, ys:List a.
  38               case xs of
  39               { Nil  => ys
  40               ; Cons x:a,xx: List a => Cons x (append xx ys)
  41               }
  42               at {a:*}
  43        }
  44
  45
  46
  47