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