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