8baaa42 · Idris-dev · git.iko.soy

CHANGELOG+4

compare with master

unifiedsplit

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

1+New in 0.9.1:

2+

3+* dsl notation

4+

10.1.x to 0.9.0:

50.1.x to 0.9.0:

2

6

3Complete rewrite. User visible changes:

7Complete rewrite. User visible changes:

idris.cabal+2−2

@@ -1,5 +1,5 @@

1Name: idris

2−Version: 0.9.0

2+Version: 0.9.1

3License: BSD3

4License-file: LICENSE

5Author: Edwin Brady

@@ -8,7 +8,7 @@ Homepage: http://www.idris-lang.org/

8

9Stability: Beta

10Category: Compilers/Interpreters, Dependent Types

11−Synopsis: Dependently Typed Functional Programming Language

11+Synopsis: Functional Programming Language with Dependent Types

12Description: Idris is a general purpose language with full dependent types.

13 It is compiled, with eager evaluation.

14 Dependent types allow types to be predicated on values,

src/Idris/Delaborate.hs+6−3

@@ -64,9 +64,12 @@ delab' ist tm fullname = de [] tm

64

65pshow :: IState -> Err -> String

66pshow i (Msg s) = s

67+pshow i (CantUnify x y e s)

67−pshow i (CantUnify x y e s) = "Can't unify " ++ show (delab i x)

68+ = "Can't unify " ++ show (delab i x)

68− ++ " with " ++ show (delab i y)

69+ ++ " with " ++ show (delab i y) ++

70+ case e of

71+ Msg "" -> ""

69−-- ++ "\n\t(" ++ pshow i e ++ ")"

72+ _ -> "\n\nSpecifically:\n\t " ++ pshow i e

70pshow i (NotInjective p x y) = "Can't verify injectivity of " ++ show (delab i p) ++

73pshow i (NotInjective p x y) = "Can't verify injectivity of " ++ show (delab i p) ++

71 " when unifying " ++ show (delab i x) ++ " and " ++

74 " when unifying " ++ show (delab i x) ++ " and " ++

72 show (delab i y)

75 show (delab i y)

tutorial/examples/Makefile+1−1

@@ -1,5 +1,5 @@

1check: .PHONY

2− rm *.ibc

2+ rm -f *.ibc

3 for x in *.idr ; do \

4 echo "Checking $$x"; \

5 idris --check $$x; \