bool : type.
true : bool.
false : bool.

nat : type.
z : nat.
succ : nat → nat.

list : nat → type.
nil : list z.
cons : bool → list N → list (succ N).

let l1 = [ ⊢ cons true nil];

let l2 = [ ⊢ cons true (cons false nil)];

rec map : (( ⊢ bool) → ( ⊢ bool)) → ( ⊢ list N) → ( ⊢ list N) =
fn f ⇒ fn l ⇒
  case l of
  | [ ⊢ nil] ⇒ [ ⊢ nil]
  | [ ⊢ cons H T] ⇒ let [ ⊢ H'] = f [ ⊢ H] in let [ ⊢ T'] = map f [ ⊢ T] in
    [ ⊢ cons H' T'];

rec head : ( ⊢ list (succ N)) → ( ⊢ bool) =
fn l ⇒ let [ ⊢ cons H _] = l in [ ⊢ H];

rec tail : ( ⊢ list (succ N)) → ( ⊢ list N) =
fn l ⇒ let [ ⊢ cons _ T] = l in [ ⊢ T];

© Computation and Logic Group
Department of Computer Science, McGill University
3480 University Street, Montreal, Quebec, Canada, H3A 0E9