1-- 2-- Copyright 2016, NICTA 3-- 4-- This software may be distributed and modified according to the terms of 5-- the GNU General Public License version 2. Note that NO WARRANTY is provided. 6-- See "LICENSE_GPLv2.txt" for details. 7-- 8-- @TAG(NICTA_GPL) 9-- 10 11type A = {f1 : X, f2 : Y, f3: Z} 12 13type X 14type Y 15type Z 16 17type B = (A take (..)) put (f1) 18-- type C = A take .. put (f1) 19-- type D = A take (.., f1) put (f1) 20-- type E = A take (f1, ..) put f1 21 22foo : () -> {f1 : X, f2 : Y, f3 : Z} take (f2, f3) 23bar : B -> () 24 25x : () -> () 26x () = bar (foo ()) 27 28-- type C = A put (f2) 29-- type D = A take (f1, f2) put (f3) 30 31-- type E = ((A take (f2)) put (f1)) take (f2) 32 33type F = (A take (f1, f2)) put (..) 34 35id : all (a). a -> a 36id x = x 37 38test : F -> A 39test y = id[A] y 40