In ML...
datatype 'a list = nil | :: of 'a * 'a list tlv
fun L t = (* 'a typ -> 'a list tlv typ *)
RR(fn D(e) => e
| S(nil) => Nil
| S(x :: y) => Cons(reify t x,
reify (L t) y),
fn e => D(e))
fun tl' (D(e)) = D(Tl(e))
| tl' (S(_ :: x)) = x
- reify (L I --> L I)
(fn a => tl' (tl' (S(S(3) :: a))));
> val it = Abs ("x1",Tl (Var "x1")) : exp
Previous slide
Next slide
Back to first slide
View graphic version