9839562 · Idris-dev · git.iko.soy

CHANGELOG+5−4

compare with master

unifiedsplit

@@ -3,15 +3,16 @@ New in 0.9.1:

3

4User visible changes:

5

6−* dsl notation

6+* DSL notation

7−* record projection and update

7+* Record projection and update

8+* Totality checking and 'total' keyword

8−* auto implicits and default argument values {auto n : T}, {default val n : T}

9+* Auto implicits and default argument values {auto n : T}, {default val n : T}

9* Additions to prelude, including Nat and List theorems

10* Additions to prelude, including Nat and List theorems

10* New libs: control.monad.identity, control.monad.state

11* New libs: control.monad.identity, control.monad.state

11

12

12Internal changes:

13Internal changes:

13

14

14−* faster compilation (only compiling names which are used)

15+* Faster compilation (only compiling names which are used)

15

16

160.1.x to 0.9.0:

170.1.x to 0.9.0:

17

18

src/Idris/Coverage.hs+1

@@ -253,6 +253,7 @@ calcTotality path fc n pats

253 Total _ -> return ords

254 p@(Partial (Mutual x)) -> return ((Left p) : ords)

255 _ -> return (Left (Partial (Other [fn])) : ords)

256+ | null args = return (Left (Partial Itself) : ords)

256 chkOrd ords args _ = return ords

257 chkOrd ords args _ = return ords

257

258

258 lexOrd x y | x == y = LexEQ

259 lexOrd x y | x == y = LexEQ

tutorial/examples/theorems.idr+17

@@ -5,6 +5,23 @@ fiveIsFive = refl

5twoPlusTwo : 2 + 2 = 4

6twoPlusTwo = refl

7

8+total imp : (n : Nat) -> O = S n -> _|_

9+imp n p = replace {P = impTy} p ()

10+ where

11+ impTy : Nat -> Set

12+ impTy O = ()

13+ impTy (S k) = _|_

14+

15+empty1 : _|_

16+empty1 = let xs : List _|_ = [] in hd xs

17+ where

18+ hd : List a -> a

19+ hd (x :: xs) = x

20+

21+

22+empty2 : _|_

23+empty2 = empty2

24+

8plusReduces : (n:Nat) -> plus O n = n

25plusReduces : (n:Nat) -> plus O n = n

9plusReduces n = refl

26plusReduces n = refl

10

27

tutorial/starting.tex+1

@@ -109,6 +109,7 @@ Idris version 0.9.1

109

110 <expr> Evaluate an expression

111 :t <expr> Check the type of an expression

112+ :total <name> Check the totality of a name

112 :r :reload Reload current file

113 :r :reload Reload current file

113 :e :edit Edit current file using $EDITOR or $VISUAL

114 :e :edit Edit current file using $EDITOR or $VISUAL

114 :m :metavars Show remaining proof obligations (metavariables)

115 :m :metavars Show remaining proof obligations (metavariables)

tutorial/theorems.tex+28

@@ -29,6 +29,34 @@ twoPlusTwo = refl

29\end{SaveVerbatim}

30\useverb{eqprf}

31

32+\subsection{The Empty Type}

33+

34+There is an empty type, \texttt{\_|\_}, which has no constructors. It is

35+therefore impossible to construct an element of the empty type, at least

36+without using a partially defined or general recursive function (see Section

37+\ref{sect:totality} for more details). We can therefore use the empty type

38+to prove that something is impossible, for example zero is never equal

39+to a successor:

40+

41+\begin{SaveVerbatim}{natdisjoint}

42+

43+imp : (n : Nat) -> O = S n -> _|_

44+imp n p = replace {P = impTy} p ()

45+ where

46+ impTy : Nat -> Set

47+ impTy O = ()

48+ impTy (S k) = _|_

49+

50+\end{SaveVerbatim}

51+\useverb{natdisjoint}

52+

53+\noindent

54+There is no need to worry too much about how this function works --- essentially,

55+it applies the library function \texttt{replace}, which uses an equality proof to

56+transform a predicate. Here we use it to transform a value of a type which can exist,

57+the empty tuple, to a value of a type which can't, by using a proof of something

58+which can't exist.

59+

32\subsection{Simple Theorems}

60\subsection{Simple Theorems}

33

61

34When type checking dependent types, the type itself gets \emph{normalised}. So imagine

62When type checking dependent types, the type itself gets \emph{normalised}. So imagine