Permalink
Browse files

Only add names once in pattern bindings

Ignore-this: b115c0b3e8c0ded86d9060c0121cd4c8
Inference will make sure they really do have the same values/types

darcs-hash:20091128133801-228f4-8039917b6df392dd7e97e24e645058de2cbd29cc.gz
  • Loading branch information...
1 parent 1a585ac commit 19089d071ed34e3ae15a30cd95e61a3173028451 eb committed Nov 28, 2009
Showing with 5 additions and 3 deletions.
  1. +5 −3 Ivor/Typecheck.lhs
View
@@ -367,12 +367,14 @@ typechecker...
> defaultResult = do
> (next, infer, bindings, errs, mvs, fc) <- get
-> if infer
-> then case exp of
+> case lookup n bindings of
+> Nothing ->
+> if infer then case exp of
> Nothing -> lift $ ifail (errCtxt fc (INoSuchVar n))
> Just (Ind t) -> do put (next, infer, (n, B Pi t):bindings, errs, mvs, fc)
> return (Ind (P n), Ind t)
-> else lift $ ifail (errCtxt fc (INoSuchVar n))
+> else lift $ ifail (errCtxt fc (INoSuchVar n))
+> Just (B Pi t) -> return (Ind (P n), Ind t)
> tc env lvl (RApp f a) exp = do
> (Ind fv, Ind ft) <- tcfixup env lvl f Nothing

0 comments on commit 19089d0

Please sign in to comment.