% Types 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] ;