Mercurial > urweb

comparison lib/ur/top.ur @ 627:f4f2b09a533a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
demo/sum working with manual folders
author Adam Chlipala <adamc@hcoop.net>
date Sun, 22 Feb 2009 17:39:55 -0500
parents 588b9d16b00a
children 12b73f3c108e
comparison
equal deleted inserted replaced
626:230654093b51 627:f4f2b09a533a
3 con folder = K ==> fn r :: {K} => 3 con folder = K ==> fn r :: {K} =>
4 tf :: ({K} -> Type) 4 tf :: ({K} -> Type)
5 -> (nm :: Name -> v :: K -> r :: {K} -> tf r 5 -> (nm :: Name -> v :: K -> r :: {K} -> tf r
6 -> fn [[nm] ~ r] => tf ([nm = v] ++ r)) 6 -> fn [[nm] ~ r] => tf ([nm = v] ++ r))
7 -> tf [] -> tf r 7 -> tf [] -> tf r
8
9 structure Folder = struct
10 fun nil K (tf :: {K} -> Type)
11 (f : nm :: Name -> v :: K -> r :: {K} -> tf r
12 -> fn [[nm] ~ r] => tf ([nm = v] ++ r))
13 (i : tf []) = i
14
15 fun cons K (r ::: {K}) (nm :: Name) (v :: K) [[nm] ~ r] (fold : folder r)
16 (tf :: {K} -> Type)
17 (f : nm :: Name -> v :: K -> r :: {K} -> tf r
18 -> fn [[nm] ~ r] => tf ([nm = v] ++ r))
19 (i : tf []) = f [nm] [v] [r] (fold [tf] f i)
20 end
8 21
9 22
10 fun not b = if b then False else True 23 fun not b = if b then False else True
11 24
12 con idT (t :: Type) = t 25 con idT (t :: Type) = t