1145522Sdarrenr-- 2145522Sdarrenr-- Copyright 2016, NICTA 353642Sguido-- 4255332Scy-- This software may be distributed and modified according to the terms of 553642Sguido-- the GNU General Public License version 2. Note that NO WARRANTY is provided. 680482Sdarrenr-- See "LICENSE_GPLv2.txt" for details. 753642Sguido-- 853642Sguido-- @TAG(NICTA_GPL) 957126Sguido-- 10172776Sdarrenr 1153642Sguidotype A = {f1 : X, f2 : Y, f3: Z} 1253642Sguido 1353642Sguido 1453642Sguidotype X 15153876Sguidotype Y 16145522Sdarrenrtype Z 1760854Sdarrenr 18145522Sdarrenrtype B = (A take (..)) put (f1) 1960854Sdarrenr-- type C = A take .. put (f1) 2060854Sdarrenrtype D = A take (.., f1) put (f1) 21145522Sdarrenr-- type E = A take (f1, ..) put f1 22145522Sdarrenr 2380482Sdarrenrfoo : () -> {f1 : X, f2 : Y, f3 : Z} take (f2, f3) 2480482Sdarrenrbar : B -> () 2580482Sdarrenr 2680482Sdarrenrx : () -> () 2780482Sdarrenrx () = bar (foo ()) 2880482Sdarrenr 2953642Sguido-- type C = A put (f2) 30255332Scy-- type D = A take (f1, f2) put (f3) 31255332Scy 32255332Scy-- type E = ((A take (f2)) put (f1)) take (f2) 33255332Scy 3453642Sguidotype F = (A take (f1, f2)) put (..) 3553642Sguido 3653642Sguidoid : all (a). a -> a 37145522Sdarrenr 3853642Sguidotest : A -> A 3960854Sdarrenrtest y = id[A] y 4060854Sdarrenr