diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2010-03-06 19:14:48 -0500 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2010-03-06 19:14:48 -0500 |
| commit | cbda10a2d0c31f366d34e059d25751fa66c3b5e5 (patch) | |
| tree | bc477781e8f3c91a920b10819bf743d10968ca88 /lib/ur/incl.urs | |
| parent | 049d85f6ec161c8df0461550549ded12be9e44e8 (diff) | |
Got split1 working, but noticed a nasty type inference bug with transplanted unification variables
Diffstat (limited to 'lib/ur/incl.urs')
| -rw-r--r-- | lib/ur/incl.urs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/ur/incl.urs b/lib/ur/incl.urs index d0d78b36..2c77369f 100644 --- a/lib/ur/incl.urs +++ b/lib/ur/incl.urs @@ -9,7 +9,7 @@ val inv1 : K --> nm :: Name -> t ::: K -> r :: {K} -> r' :: {K} -> incl ([nm = t] ++ r) r' -> (nm :: Name -> t :: K -> r :: {K} -> [[nm] ~ r] => f nm t ([nm = t] ++ r)) -> f nm t r' -val inv2 : K --> nm :: Name -> t ::: K -> r :: {K} -> r' :: {K} +val inv2 : K --> nm :: Name -> t :: K -> r :: {K} -> r' :: {K} -> [[nm] ~ r] => incl ([nm = t] ++ r) r' -> incl r r' |