Mercurial > urweb
comparison lib/ur/mem.ur @ 1182:0b1d666bddb4
Spiffed-up Split1; remove spurious error message triggered by 'open'ing a module containing a functor
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 09 Mar 2010 17:50:42 -0500 |
parents | ac3dbbc85c6e |
children |
comparison
equal
deleted
inserted
replaced
1181:618f9f458da9 | 1182:0b1d666bddb4 |
---|---|
32 (f : nm :: Name -> v :: K -> r' :: {K} -> [[nm] ~ r'] | 32 (f : nm :: Name -> v :: K -> r' :: {K} -> [[nm] ~ r'] |
33 => mem nm v r -> tf r' -> tf ([nm = v] ++ r')) | 33 => mem nm v r -> tf r' -> tf ([nm = v] ++ r')) |
34 (i : tf []) (fl : folder r) = | 34 (i : tf []) (fl : folder r) = |
35 @@Incl.fold [tf] [r] | 35 @@Incl.fold [tf] [r] |
36 (fn [nm :: Name] [v :: K] [r' :: {K}] [[nm] ~ r'] (i : Incl.incl ([nm = v] ++ r') r) acc => | 36 (fn [nm :: Name] [v :: K] [r' :: {K}] [[nm] ~ r'] (i : Incl.incl ([nm = v] ++ r') r) acc => |
37 f [nm] [v] [r'] ! (Incl.inv1 [nm] [r'] [r] [mem] i mem) acc) | 37 f [nm] [v] [r'] ! (Incl.inv1 [nm] [v] [r'] [r] [mem] i mem) acc) |
38 i fl | 38 i fl |