Merge pull request #528 from ahmadsalim/master
Improvement regarding parsing of slices, and addproof syntax
commita51ed3dbc53749310546acf9e6d8e8122a231272
authorEdwin Brady <edwin.brady@gmail.com>
dateSun 13 Oct 2013, 16:09 (13 years ago)
parent6367eb5267f34d
src/Idris/ParseExpr.hs+1−1
@@ -324,7 +324,7 @@ bracketed syn =
324324 lchar ')'
325325 return (PDPair fc l Placeholder r)
326326 <|> try(do fc0 <- getFC
327− l <- simpleExpr syn
327+ l <- expr' syn
328328 o <- operator
329329 lchar ')'
330330 return $ PLam (MN 1000 "ARG") Placeholder
src/Idris/Prover.hs+3−3
@@ -37,9 +37,9 @@ prover lit x =
3737
3838showProof :: Bool -> Name -> [String] -> String
3939showProof lit n ps
40− = bird ++ show n ++ " = proof {" ++ break ++
41− showSep break (map (\x -> " " ++ x ++ ";") ps) ++
42− break ++ "}\n"
40+ = bird ++ show n ++ " = proof" ++ break ++
41+ showSep break (map (\x -> " " ++ x) ps) ++
42+ break ++ "\n"
4343 where bird = if lit then "> " else ""
4444 break = "\n" ++ bird
4545