Mercurial > urweb

comparison lib/ur/incl.ur @ 1182:0b1d666bddb4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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 618f9f458da9
children
comparison
equal deleted inserted replaced
1181:618f9f458da9 1182:0b1d666bddb4
12 12
13 fun proj [r1 ::: {Type}] [r2 ::: {Type}] (i : incl r1 r2) (r : $r2) = 13 fun proj [r1 ::: {Type}] [r2 ::: {Type}] (i : incl r1 r2) (r : $r2) =
14 i [$r1] (fn [r' :: {Type}] [r1 ~ r'] (i' : incl' r1 r2 r') => 14 i [$r1] (fn [r' :: {Type}] [r1 ~ r'] (i' : incl' r1 r2 r') =>
15 i'.Expose [fn r => $r] r --- r') 15 i'.Expose [fn r => $r] r --- r')
16 16
17 fun inv1 [K] [nm :: Name] [t ::: K] [r :: {K}] [r' :: {K}] [[nm] ~ r] 17 fun inv1 [K] [nm :: Name] [t :: K] [r :: {K}] [r' :: {K}] [[nm] ~ r]
18 [f :: Name -> K -> {K} -> Type] 18 [f :: Name -> K -> {K} -> Type]
19 (i : incl ([nm = t] ++ r) r') 19 (i : incl ([nm = t] ++ r) r')
20 (f : nm :: Name -> t :: K -> r :: {K} -> [[nm] ~ r] => f nm t ([nm = t] ++ r)) = 20 (f : nm :: Name -> t :: K -> r :: {K} -> [[nm] ~ r] => f nm t ([nm = t] ++ r)) =
21 i [f nm t r'] (fn [r'' :: {K}] [[nm = t] ++ r ~ r''] (i' : incl' ([nm = t] ++ r) r' r'') => 21 i [f nm t r'] (fn [r'' :: {K}] [[nm = t] ++ r ~ r''] (i' : incl' ([nm = t] ++ r) r' r'') =>
22 i'.Hide [f nm t] (f [nm] [t] [r ++ r''] !)) 22 i'.Hide [f nm t] (f [nm] [t] [r ++ r''] !))