comparison lib/ur/top.ur @ 650:fcf0bd3d1667

BatchG demo
author Adam Chlipala <adamc@hcoop.net>
date Tue, 10 Mar 2009 16:38:38 -0400
parents aa2290c32ce2
children e5894f0e541a
comparison
equal deleted inserted replaced
649:96ebc6bdb5a0 650:fcf0bd3d1667
5 -> (nm :: Name -> v :: K -> r :: {K} -> tf r 5 -> (nm :: Name -> v :: K -> r :: {K} -> tf r
6 -> [[nm] ~ r] => tf ([nm = v] ++ r)) 6 -> [[nm] ~ r] => tf ([nm = v] ++ r))
7 -> tf [] -> tf r 7 -> tf [] -> tf r
8 8
9 structure Folder = struct 9 structure Folder = struct
10 fun fold K (r ::: {K}) (fl : folder r) = fl 10 fun fold K (r :: {K}) (fl : folder r) = fl
11 11
12 fun nil K (tf :: {K} -> Type) 12 fun nil K (tf :: {K} -> Type)
13 (f : nm :: Name -> v :: K -> r :: {K} -> tf r 13 (f : nm :: Name -> v :: K -> r :: {K} -> tf r
14 -> [[nm] ~ r] => tf ([nm = v] ++ r)) 14 -> [[nm] ~ r] => tf ([nm = v] ++ r))
15 (i : tf []) = i 15 (i : tf []) = i