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