Mercurial > urweb

annotate tests/stuff.ur @ 1244:1eedc9086e6c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Use key information in more places, and catch cases where one key completion depends on another having happened already
author Adam Chlipala <adamc@hcoop.net>
date Sun, 18 Apr 2010 13:00:36 -0400
parents 71bafe66dbe1
children
rev   line source
adamc@7 1 type c1 = t :: Type -> t
adamc@1 2 con c2 :: Type = t :: Type -> t
adamc@1 3 con c3 = fn t :: Type => c1
adamc@1 4 con c4 = c3 c1
adamc@1 5 con c5 = (fn t :: Type => c1) c1
adamc@1 6
adamc@1 7 con name = #MyName
adamc@1 8
adamc@1 9 con c6 = {A : c1, name : c2}
adamc@1 10 con c7 = [A = c1, name = c2]
adamc@5 11
adamc@5 12 con c8 = fn t :: Type => t
adamc@6 13
adamc@6 14 con c9 = {}
adamc@6 15 con c10 = ([]) :: {Type}
adamc@8 16
adamc@8 17 val v1 = fn t :: Type => fn x : t => x
adamc@11 18 val v2 = v1 [t :: Type -> t -> t] v1
adamc@12 19
adamc@12 20 val r = {X = v1, Y = v2}
adamc@12 21 val v1_again = r.X
adamc@12 22 val v2_again = r.Y
adamc@12 23
adamc@12 24 val r2 = {X = {}, Y = v2, Z = {}}
adamc@12 25 val r2_X = r2.X
adamc@12 26 val r2_Y = r2.Y
adamc@12 27 val r2_Z = r2.Z
adamc@12 28
adamc@12 29 val f = fn fs :: {Type} => fn x : $([X = {}] ++ fs) => x.X
adamc@12 30 val f2 = fn fs :: {Type} => fn x : $(fs ++ [X = {}]) => x.X
adamc@12 31 val f3 = fn fs :: {Type} => fn x : $([X = {}, Y = {Z : {}}] ++ fs) => x.X
adamc@12 32 val f4 = fn fs :: {Type} => fn x : $([X = {}, Y = {Z : {}}] ++ fs) => x.Y
adamc@12 33 val f5 = fn fs1 :: {Type} => fn fs2 :: {Type} => fn x : $(fs1 ++ [X = {}] ++ fs2) => x.X
adamc@12 34 val f6 = fn fs1 :: {Type} => fn fs2 :: {Type} => fn x : $(fs1 ++ [X = {}] ++ fs2 ++ [Y = {Z : {}}]) => x.X
adamc@12 35 val f7 = fn fs1 :: {Type} => fn fs2 :: {Type} => fn x : $(fs1 ++ [X = {}] ++ fs2 ++ [Y = {Z : {}}]) => x.Y
adamc@12 36
adamc@12 37 val test = f [[Y = t :: Type -> t -> t, Z = {}]] r2
adamc@12 38 val test = f7 [[Y = t :: Type -> t -> t]] [[Z = {}]] r2