Mercurial > urweb
annotate tests/reduce.lac @ 21:067029c748e9
Beta reductions for expressions
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 08 Jun 2008 16:02:26 -0400 |
parents | 1ab48e37d0ef |
children | d8850cc06d24 |
rev | line source |
---|---|
adamc@20 | 1 con c1 = int |
adamc@20 | 2 con c2 = (fn t :: Type => t) int |
adamc@20 | 3 |
adamc@20 | 4 con id = fn t :: Type => t |
adamc@20 | 5 con c3 = id int |
adamc@20 | 6 |
adamc@20 | 7 con fst = fn t1 :: Type => fn t2 :: Type => t1 |
adamc@20 | 8 con c4 = fst int string |
adamc@20 | 9 |
adamc@20 | 10 con snd = fn t1 :: Type => fn t2 :: Type => t2 |
adamc@20 | 11 con c5 = snd int string |
adamc@20 | 12 |
adamc@20 | 13 con apply = fn f :: Type -> Type => fn t :: Type => f t |
adamc@20 | 14 con c6 = apply id int |
adamc@20 | 15 con c7 = apply (fst int) string |
adamc@20 | 16 |
adamc@20 | 17 val grab = fn n :: Name => fn t :: Type => fn fs :: {Type} => |
adamc@20 | 18 fn x : $([n = t] ++ fs) => x |
adamc@20 | 19 val grabA = grab[#A][int][[B = string]] |
adamc@21 | 20 val test_grabA = grabA {A = 6, B = "13"} |