Mercurial > urweb
comparison lib/ur/incl.urs @ 1181:618f9f458da9
Got split1 working, but noticed a nasty type inference bug with transplanted unification variables
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sat, 06 Mar 2010 19:14:48 -0500 |
parents | ac3dbbc85c6e |
children | 0b1d666bddb4 |
comparison
equal
deleted
inserted
replaced
1180:ac3dbbc85c6e | 1181:618f9f458da9 |
---|---|
7 -> [[nm] ~ r] => | 7 -> [[nm] ~ r] => |
8 f :: (Name -> K -> {K} -> Type) | 8 f :: (Name -> K -> {K} -> Type) |
9 -> incl ([nm = t] ++ r) r' | 9 -> incl ([nm = t] ++ r) r' |
10 -> (nm :: Name -> t :: K -> r :: {K} -> [[nm] ~ r] => f nm t ([nm = t] ++ r)) | 10 -> (nm :: Name -> t :: K -> r :: {K} -> [[nm] ~ r] => f nm t ([nm = t] ++ r)) |
11 -> f nm t r' | 11 -> f nm t r' |
12 val inv2 : K --> nm :: Name -> t ::: K -> r :: {K} -> r' :: {K} | 12 val inv2 : K --> nm :: Name -> t :: K -> r :: {K} -> r' :: {K} |
13 -> [[nm] ~ r] => | 13 -> [[nm] ~ r] => |
14 incl ([nm = t] ++ r) r' -> incl r r' | 14 incl ([nm = t] ++ r) r' -> incl r r' |
15 | 15 |
16 val fold : K --> tf :: ({K} -> Type) -> r ::: {K} | 16 val fold : K --> tf :: ({K} -> Type) -> r ::: {K} |
17 -> (nm :: Name -> v :: K -> r' :: {K} | 17 -> (nm :: Name -> v :: K -> r' :: {K} |