Changed the way addproof works to indented-block style
Allowed a larger range of expression to work with slices (improves on
idris-lang/Idris-dev#524)
commit267f34dbedb0f29ab2786cbfadc7662b562c41c5
authorAhmad Salim Al-Sibahi <asal@itu.dk>
dateThu 10 Oct 2013, 15:08 (13 years ago)
parent54a89bf
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