Mercurial > urweb
comparison tests/reduce.lac @ 22:d8850cc06d24
Reducing known record projections
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 08 Jun 2008 16:08:31 -0400 |
parents | 067029c748e9 |
children | bfa2e9ae4df8 |
comparison
equal
deleted
inserted
replaced
21:067029c748e9 | 22:d8850cc06d24 |
---|---|
12 | 12 |
13 con apply = fn f :: Type -> Type => fn t :: Type => f t | 13 con apply = fn f :: Type -> Type => fn t :: Type => f t |
14 con c6 = apply id int | 14 con c6 = apply id int |
15 con c7 = apply (fst int) string | 15 con c7 = apply (fst int) string |
16 | 16 |
17 val grab = fn n :: Name => fn t :: Type => fn fs :: {Type} => | 17 val tickle = fn n :: Name => fn t :: Type => fn fs :: {Type} => |
18 fn x : $([n = t] ++ fs) => x | 18 fn x : $([n = t] ++ fs) => x |
19 val grabA = grab[#A][int][[B = string]] | 19 val tickleA = tickle[#A][int][[B = string]] |
20 val test_grabA = grabA {A = 6, B = "13"} | 20 val test_tickleA = tickleA {A = 6, B = "13"} |
21 | |
22 val grab = fn n :: Name => fn t ::: Type => fn fs ::: {Type} => | |
23 fn x : $([n = t] ++ fs) => x.n | |
24 val test_grab1 = grab[#A] {A = 6, B = "13"} | |
25 val test_grab2 = grab[#B] {A = 6, B = "13"} |