Mercurial > urweb
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 |