summaryrefslogtreecommitdiff
path: root/tests/reduce.lac
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-06-08 16:08:31 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-06-08 16:08:31 -0400
commitd52cd67621a27bbd27888c170c843fafb552658c (patch)
treeda9a0932b4510bfb29a492314912c4e4aa84b73b /tests/reduce.lac
parent813e9aa4d196962f47c784aeedeaf1cddf54dc4f (diff)
Reducing known record projections
Diffstat (limited to 'tests/reduce.lac')
-rw-r--r--tests/reduce.lac11
1 files changed, 8 insertions, 3 deletions
diff --git a/tests/reduce.lac b/tests/reduce.lac
index 2585862d..9cdc2a1a 100644
--- a/tests/reduce.lac
+++ b/tests/reduce.lac
@@ -14,7 +14,12 @@ con apply = fn f :: Type -> Type => fn t :: Type => f t
con c6 = apply id int
con c7 = apply (fst int) string
-val grab = fn n :: Name => fn t :: Type => fn fs :: {Type} =>
+val tickle = fn n :: Name => fn t :: Type => fn fs :: {Type} =>
fn x : $([n = t] ++ fs) => x
-val grabA = grab[#A][int][[B = string]]
-val test_grabA = grabA {A = 6, B = "13"}
+val tickleA = tickle[#A][int][[B = string]]
+val test_tickleA = tickleA {A = 6, B = "13"}
+
+val grab = fn n :: Name => fn t ::: Type => fn fs ::: {Type} =>
+ fn x : $([n = t] ++ fs) => x.n
+val test_grab1 = grab[#A] {A = 6, B = "13"}
+val test_grab2 = grab[#B] {A = 6, B = "13"}