Mercurial > urweb
annotate tests/reduce.ur @ 352:2205d5cb416a
Get type definitions font-locking again
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 12 Oct 2008 10:30:08 -0400 |
parents | 71bafe66dbe1 |
children |
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@22 | 17 val tickle = fn n :: Name => fn t :: Type => fn fs :: {Type} => |
adamc@20 | 18 fn x : $([n = t] ++ fs) => x |
adamc@22 | 19 val tickleA = tickle[#A][int][[B = string]] |
adamc@22 | 20 val test_tickleA = tickleA {A = 6, B = "13"} |
adamc@22 | 21 |
adamc@22 | 22 val grab = fn n :: Name => fn t ::: Type => fn fs ::: {Type} => |
adamc@22 | 23 fn x : $([n = t] ++ fs) => x.n |
adamc@22 | 24 val test_grab1 = grab[#A] {A = 6, B = "13"} |
adamc@22 | 25 val test_grab2 = grab[#B] {A = 6, B = "13"} |
adamc@23 | 26 |
adamc@23 | 27 val main = {A = test_grab1, B = test_grab2} |