type List<x> LEOF | (LCons( x , List<x>[] )); zero List<x> LEOF;

cons := λ(: hd x)(: tl List<x>). (: (
   (set tl (LCons( hd (close tl) )))
   tl
) List<x>);

head := λ(: l List<x>). (: (
   (match l (
      ()
      ( LEOF (fail 'List::head\sis\sfallible\n_s) )
      ( _ () )
   ))
   (.2(as l List<x>+Tag<LCons>))
) x);

+ := λ(: hd List<x>)(: tl List<x>). (: (
   (set hd (reverse hd))
   (while (non-zero hd) (match hd (
      ()
      ( (LCons( hdhd tlhd )) (
         (set tl (cons( hdhd tl )))
         (set hd tlhd)
      ))
   )))
   tl
) List<x>);

.length := λ(: list List<x>). (: (
   (let l 0_u64)
   (while (non-zero list) (
      (match list (
         ()
         ( (LCons( _ tl )) (set list tl) )
      ))
      (set l (+( l 1_u64 )))
   ))
   l
) U64);

reverse := λ(: l List<x>). (: (
   (let r (: LEOF List<x>))
   (while (non-zero l) (match l (
      ()
      ( (LCons( v rst )) (
         (set r (LCons( v (close r) )))
         (set l rst)
      ))
   )))
   r
) List<x>);

print := λ(: l List<x>). (: (
   (print '[_s)
   (let some False_u8)
   (while (non-zero l) (match l (
      ()
      ( (LCons( v rst )) (
         (if (==( some True_u8 )) (print ',_s) ())
         (print v)
         (set some True_u8)
         (set l rst)
      ))
   )))
   (print ']_s)
) Nil);

.nth := λ(: tt List<x>)(: i U64)(: default x). (: (
   (while (>( i 0_u64 )) (
      (match tt (
         ()
         ( (LCons( _ rst )) (set tt rst) )
         ( _ () )
      ))
      (set i (-( i 1_u64 )))
   ))
   (match tt (
      ()
      ( (LCons( d _ )) (set default d) )
      ( _ () )
   ))
   default
) Type);