Mercurial > urweb
comparison lib/ur/top.urs @ 628:12b73f3c108e
Switch to TDisjoint from CDisjoint; still need to implement obligation generation at EDisjoint uses
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 24 Feb 2009 12:01:24 -0500 |
parents | f4f2b09a533a |
children | e68de2a5506b |
comparison
equal
deleted
inserted
replaced
627:f4f2b09a533a | 628:12b73f3c108e |
---|---|
8 | 8 |
9 structure Folder : sig | 9 structure Folder : sig |
10 val nil : K --> folder (([]) :: {K}) | 10 val nil : K --> folder (([]) :: {K}) |
11 val cons : K --> r ::: {K} -> nm :: Name -> v :: K | 11 val cons : K --> r ::: {K} -> nm :: Name -> v :: K |
12 -> fn [[nm] ~ r] => folder r -> folder ([nm = v] ++ r) | 12 -> fn [[nm] ~ r] => folder r -> folder ([nm = v] ++ r) |
13 val concat : K --> r1 ::: {K} -> r2 ::: {K} | |
14 -> fn [r1 ~ r2] => folder r1 -> folder r2 -> folder (r1 ++ r2) | |
13 end | 15 end |
14 | 16 |
15 | 17 |
16 val not : bool -> bool | 18 val not : bool -> bool |
17 | 19 |