Mercurial > urweb
comparison lib/ur/top.ur @ 631:effa7d43aac3
Make folders abstract
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 24 Feb 2009 14:04:07 -0500 |
parents | 6a6eb9882d57 |
children | 6c4643880df5 |
comparison
equal
deleted
inserted
replaced
630:6a6eb9882d57 | 631:effa7d43aac3 |
---|---|
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 | |
11 | |
10 fun nil K (tf :: {K} -> Type) | 12 fun nil K (tf :: {K} -> Type) |
11 (f : nm :: Name -> v :: K -> r :: {K} -> tf r | 13 (f : nm :: Name -> v :: K -> r :: {K} -> tf r |
12 -> [[nm] ~ r] => tf ([nm = v] ++ r)) | 14 -> [[nm] ~ r] => tf ([nm = v] ++ r)) |
13 (i : tf []) = i | 15 (i : tf []) = i |
14 | 16 |