865bf99 · Idris-dev · git.iko.soy

libs/prelude/Prelude.idr+2−2

@@ -275,11 +275,11 @@ instance Applicative List where

275instance Applicative (Vect k) where

276 pure = replicate _

277

278− fs <$> vs = zipWith ($) fs vs

278+ fs <$> vs = zipWith apply fs vs

279

280instance Applicative Stream where

281 pure = repeat

282− (<$>) = zipWith ($)

282+ (<$>) = zipWith apply

283

284---- Alternative instances

285

libs/prelude/Prelude/Basics.idr+2−4

@@ -33,11 +33,9 @@ infixl 9 .

33flip : (a -> b -> c) -> b -> a -> c

34flip f x y = f y x

35

36−infixr 1 $

37−

38-- | Function application.

36-- | Function application.

39−($) : (a -> b) -> a -> b

37+apply : (a -> b) -> a -> b

40−f $ a = f a

38+apply f a = f a

41

39

42cong : {f : t -> u} -> (a = b) -> f a = f b

40cong : {f : t -> u} -> (a = b) -> f a = f b

43cong refl = refl

41cong refl = refl

src/Idris/ParseOps.hs+1

@@ -37,6 +37,7 @@ table fixes

37 [pexp (PApp fc (PRef fc (sUN "fromInteger")) [pexp (PConstant (BI 0))]), pexp x])]]

38 ++ toTable (reverse fixes) ++

39 [[backtick],

40+ [binary "$" (\fc x y -> PApp fc x [pexp y]) AssocRight],

40 [binary "=" PEq AssocLeft],

41 [binary "=" PEq AssocLeft],

41 [binary "->" (\fc x y -> PPi expl (sMN 42 "__pi_arg") x y) AssocRight]]

42 [binary "->" (\fc x y -> PPi expl (sMN 42 "__pi_arg") x y) AssocRight]]

42

43