e9127ba · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Restored "__pi_arg" to use UN instead of MN again (due to a test

e9127baAhmad Salim Al-Sibahi13 years ago

src/Idris/ParseExpr.hs+1−1

@@ -801,7 +801,7 @@ pi syn =

801 <|> (do x <- opExpr syn

802 (do symbol "->"

803 sc <- expr syn

804− return (PPi (Exp opts st False) (sMN 0 "__pi_arg") x sc))

804+ return (PPi (Exp opts st False) (sUN "__pi_arg") x sc))

805 <|> return x)

806 <?> "dependent type signature"

807

src/Idris/ParseOps.hs+1−2

@@ -38,8 +38,7 @@ table fixes

38 ++ toTable (reverse fixes) ++

39 [[backtick],

40 [binary "$" (\fc x y -> flatten $ PApp fc x [pexp y]) AssocRight],

41− [binary "=" PEq AssocLeft]] --,

41+ [binary "=" PEq AssocLeft]]

42− -- [binary "->" (\fc x y -> PPi expl (sUN "__pi_arg") x y) AssocRight]]

43 where

42 where

44 flatten :: PTerm -> PTerm -- flatten application

43 flatten :: PTerm -> PTerm -- flatten application

45 flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))

44 flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))