624d6c7 · Idris-dev · git.iko.soy

idris.cabal+2

@@ -235,6 +235,8 @@ Extra-source-files:

235 test/reg042/run

236 test/reg042/*.idr

237 test/reg042/expected

238+ test/reg043/run

239+ test/reg043/expected

238

240

239 test/basic001/run

241 test/basic001/run

240 test/basic001/*.idr

242 test/basic001/*.idr

src/Idris/AbsSyntaxTree.hs+2−2

@@ -1193,7 +1193,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1193 st <> text "->" <$> prettySe 10 ((n, False):bnd) sc

1194 | otherwise =

1195 bracket p 2 . group $

1196− group (prettySe 0 bnd ty <+> st) <> text "->" <$> group (prettySe 10 ((n, False):bnd) sc)

1196+ group (prettySe 1 bnd ty <+> st) <> text "->" <$> group (prettySe 10 ((n, False):bnd) sc)

1197 where

1198 st =

1199 case s of

@@ -1253,7 +1253,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1253 | PConstant (Idris.Core.TT.Str str) <- getTm tm,

1254 f == sUN "Symbol_" = annotate AnnConstType $

1255 char '\'' <> prettySe 10 bnd (PRef fc (sUN str))

1256− prettySe p bnd (PApp _ f as) =

1256+ prettySe p bnd (PApp _ f as) = -- Normal prefix applications

1257 let args = getExps as

1258 fp = prettySe 1 bnd f

1259 in

test/reg041/expected+1−1

@@ -1,3 +1,3 @@

1Type checking ./ott.idr

2−?prf : (x : Bool) -> (x1 : Bool) -> (El (EQ two x two x1)) -> El (EQ two x two x1)

2+?prf : (x : Bool) -> (x1 : Bool) -> El (EQ two x two x1) -> El (EQ two x two x1)

3Z

test/reg043/expectednew file+1

@@ -0,0 +1 @@

1+take : (m : Fin 3) -> Vect 2 Nat -> Vect (finToNat m) Nat

test/reg043/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris $@ --nocolour -e "Vect.take {n=2} {a=Nat}"

3+