git.iko.soy/Idris-dev
on master help sign in
Use correct fixity info for :printdef
13ad7deDavid Raymond Christiansen
src/Idris/REPL.hs+1−1
compare with master
unifiedsplit
@@ -1512,7 +1512,7 @@ pprintDef asCore n =
1512 let ppTm t = annotate (AnnTerm (zip vars (repeat False)) t) .
1512 let ppTm t = annotate (AnnTerm (zip vars (repeat False)) t) .
1513 pprintPTerm (ppOptionIst ist)
1513 pprintPTerm (ppOptionIst ist)
1514 (zip vars (repeat False))
1514 (zip vars (repeat False))
1515− [] [] .
1515+ [] (idris_infixes ist) .
1516 delab ist $
1516 delab ist $
1517 t
1517 t
1518 in group $ ppTm lhs <+> text "=" <$> (group . align . hang 2 $ ppTm rhs)
1518 in group $ ppTm lhs <+> text "=" <$> (group . align . hang 2 $ ppTm rhs)
test/delab001/expected+2−2
@@ -5,8 +5,8 @@ foo n = case n of
5bar : Nat -> String -> String
5bar : Nat -> String -> String
6bar x y = case x of
6bar x y = case x of
7 0 => y
7 0 => y
8− S _ => (y ++ y)
8+ S _ => y ++ y
9append : List a -> List a -> List a
9append : List a -> List a -> List a
10append xs ys = case xs of
10append xs ys = case xs of
11 [] => ys
11 [] => ys
12− (x :: xs) => (x :: (append xs ys))
12+ x :: xs => x :: append xs ys