comparison lib/ur/top.urs @ 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
1 (** Row folding *) 1 (** Row folding *)
2 2
3 con folder :: K --> {K} -> Type 3 con folder :: K --> {K} -> Type
4 4
5 structure Folder : sig 5 structure Folder : sig
6 val fold : K --> r ::: {K} -> folder r 6 val fold : K --> r :: {K} -> folder r
7 -> tf :: ({K} -> Type) 7 -> tf :: ({K} -> Type)
8 -> (nm :: Name -> v :: K -> r :: {K} -> tf r 8 -> (nm :: Name -> v :: K -> r :: {K} -> tf r
9 -> [[nm] ~ r] => tf ([nm = v] ++ r)) 9 -> [[nm] ~ r] => tf ([nm = v] ++ r))
10 -> tf [] -> tf r 10 -> tf [] -> tf r
11 11