Mercurial > urweb

comparison lib/ur/top.urs @ 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 : sig
10 val nil : K --> folder (([]) :: {K})
11 val cons : K --> r ::: {K} -> nm :: Name -> v :: K
12 -> fn [[nm] ~ r] => folder r -> folder ([nm = v] ++ r)
13 end
8 14
9 15
10 val not : bool -> bool 16 val not : bool -> bool
11 17
12 con idT = fn t :: Type => t 18 con idT = fn t :: Type => t