Restored "__pi_arg" to use UN instead of MN again (due to a test
failure).
Removed commented out code.
commite9127bada67b2e2ddec9b90733ab28666dc36f6c
authorAhmad Salim Al-Sibahi <asal@itu.dk>
dateThu 24 Apr 2014, 11:14 (13 years ago)
parentd28c82f
src/Idris/ParseExpr.hs+1−1
@@ -801,7 +801,7 @@ pi syn =
801801 <|> (do x <- opExpr syn
802802 (do symbol "->"
803803 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))
805805 <|> return x)
806806 <?> "dependent type signature"
807807
src/Idris/ParseOps.hs+1−2
@@ -38,8 +38,7 @@ table fixes
3838 ++ toTable (reverse fixes) ++
3939 [[backtick],
4040 [binary "$" (\fc x y -> flatten $ PApp fc x [pexp y]) AssocRight],
41− [binary "=" PEq AssocLeft]] --,
42− -- [binary "->" (\fc x y -> PPi expl (sUN "__pi_arg") x y) AssocRight]]
41+ [binary "=" PEq AssocLeft]]
4342 where
4443 flatten :: PTerm -> PTerm -- flatten application
4544 flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))