Mercurial > urweb

comparison lib/ur/top.ur @ 628:12b73f3c108e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
15 fun cons K (r ::: {K}) (nm :: Name) (v :: K) [[nm] ~ r] (fold : folder r) 15 fun cons K (r ::: {K}) (nm :: Name) (v :: K) [[nm] ~ r] (fold : folder r)
16 (tf :: {K} -> Type) 16 (tf :: {K} -> Type)
17 (f : nm :: Name -> v :: K -> r :: {K} -> tf r 17 (f : nm :: Name -> v :: K -> r :: {K} -> tf r
18 -> fn [[nm] ~ r] => tf ([nm = v] ++ r)) 18 -> fn [[nm] ~ r] => tf ([nm = v] ++ r))
19 (i : tf []) = f [nm] [v] [r] (fold [tf] f i) 19 (i : tf []) = f [nm] [v] [r] (fold [tf] f i)
20
21 fun concat K (r1 ::: {K}) (r2 ::: {K}) [r1 ~ r2]
22 (f1 : folder r1) (f2 : folder r2)
23 (tf :: {K} -> Type)
24 (f : nm :: Name -> v :: K -> r :: {K} -> tf r
25 -> fn [[nm] ~ r] => tf ([nm = v] ++ r))
26 (i : tf []) =
27 f1 [fn r1' [r1' ~ r2] => tf (r1' ++ r2)] 0
28 (*(fn (nm :: Name) (v :: K) (r1' :: {K}) (acc : fn [r1' ~ r2] => tf (r1' ++ r2))
29 [[nm] ~ r1'] [[nm = v] ++ r1' ~ r2] =>
30 f [nm] [v] [r1' ++ r2] acc)
31 (f2 [tf] f i)*)
20 end 32 end
21 33
22 34
23 fun not b = if b then False else True 35 fun not b = if b then False else True
24 36