e8596bc · Idris-dev · git.iko.soy

CHANGELOG.md+3

compare with master

unifiedsplit

@@ -22,6 +22,9 @@

22 with a (strictly) smaller `size`.

23

24 A good example of this idiom at work is `Data.List.Views.splitRec` from `base`.

25++ Added utility lemma `decEqSelfIsYes : decEq x x = Yes Refl` to

26+ `Decidable.Equality`. This is primarily useful for proving properties of

27+ functions defined with the help of `decEq`.

25

28

26## Tool Updates

29## Tool Updates

27

30

docs/reference/elaborator-reflection.rst+6−1

@@ -32,6 +32,9 @@ Running Elaborator Scripts

32

33On their own, tactics have no effect.

34The meta-operation ``%runElab script`` runs ``script`` in the current elaboration context.

35+Before you can use ``%runElab``, you will have to enable the language extension by adding

36+``%language ElabReflection`` in your file (or by passing ``-X ElabReflection`` to the

37+``idris`` executable from your command line).

35For example, the following script constructs the identity function at type ``Nat``:

38For example, the following script constructs the identity function at type ``Nat``:

36

39

37.. code-block:: idris

40.. code-block:: idris

@@ -88,7 +91,9 @@ that fills the hole.

88

91

89The interactive elaboration shell accepts a limited number of commands,

92The interactive elaboration shell accepts a limited number of commands,

90including a subset of the commands understood by the normal Idris REPL

93including a subset of the commands understood by the normal Idris REPL

91−as well as some elaboration-specific commands.

94+as well as some elaboration-specific commands. It also supports the

95+``do``-syntax, meaning you can write ``res <- command`` to bind the result of

96+``command`` to variable ``res``.

92

97

93General-purpose commands:

98General-purpose commands:

94

99

docs/reference/ide-protocol.rst+1−4

@@ -51,9 +51,6 @@ The available commands include:

51 ``(:interpret STRING)``

52 Interpret ``STRING`` at the Idris REPL, returning a highlighted result.

53

54− ``(:repl-completions STRING)``

55− Return the result of tab-completing ``STRING`` as a REPL command.

56−

57 ``(:type-of STRING)``

54 ``(:type-of STRING)``

58 Return the type of the name, written with Idris syntax in the ``STRING``.

55 Return the type of the name, written with Idris syntax in the ``STRING``.

59 The reply may contain highlighting information.

56 The reply may contain highlighting information.

@@ -122,7 +119,7 @@ The available commands include:

122 Return the definition of ``NAME`` as a highlighted string.

119 Return the definition of ``NAME`` as a highlighted string.

123

120

124 ``(:repl-completions NAME)``

121 ``(:repl-completions NAME)``

125− Search names, types and documentations which contain ``NAME``.

122+ Search names, types and documentations which contain ``NAME``. Return the result of tab-completing ``NAME`` as a REPL command.

126

123

127 ``:version``

124 ``:version``

128 Return the version information of the Idris compiler.

125 Return the version information of the Idris compiler.

docs/reference/syntax-guide.rst+7−1

@@ -387,10 +387,16 @@ Totality

387::

388

389 total

390− implicit

391 partial

390 partial

392 covering

391 covering

393

392

393+Implicit Coercion

394+^^^^^^^^^^^^^^^^^

395+

396+::

397+

398+ implicit

399+

394Options

400Options

395^^^^^^^

401^^^^^^^

396

402

docs/tutorial/interfaces.rst+2−2

@@ -48,8 +48,8 @@ For example, the

48Only one implementation of an interface can be given for a type — implementations may

49not overlap. Implementation declarations can themselves have constraints.

50To help with resolution, the arguments of an implementation must be

51−constructors (either data or type constructors), variables or

51+constructors (either data or type constructors) or variables

52−constants (i.e. you cannot give an implementation for a function). For

52+(i.e. you cannot give an implementation for a function). For

53example, to define a ``Show`` implementation for vectors, we need to know

54that there is a ``Show`` implementation for the element type, because we are

55going to use it to convert each element to a ``String``:

libs/contrib/Data/Heap.idr−4

@@ -132,10 +132,6 @@ implementation Ord a => Monoid (MaxiphobicHeap a) where

132-- Properties

133--------------------------------------------------------------------------------

134

135−total

136−absurdBoolDischarge : False = True -> Void

137−absurdBoolDischarge Refl impossible

138−

139total

135total

140isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = Z

136isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = Z

141isEmptySizeZero Empty p = Refl

137isEmptySizeZero Empty p = Refl

libs/prelude/Decidable/Equality.idr+15−9

@@ -8,18 +8,10 @@ import Prelude.Either

8import Prelude.List

9import Prelude.Nat

10import Prelude.Maybe

11+import Prelude.Uninhabited

11

12

12%access public export

13%access public export

13

14

14−--------------------------------------------------------------------------------

15−-- Utility lemmas

16−--------------------------------------------------------------------------------

17−

18−||| The negation of equality is symmetric (follows from symmetry of equality)

19−total negEqSym : {a : t} -> {b : t} -> (a = b -> Void) -> (b = a -> Void)

20−negEqSym p h = p (sym h)

21−

22−

23--------------------------------------------------------------------------------

15--------------------------------------------------------------------------------

24-- Decidable equality

16-- Decidable equality

25--------------------------------------------------------------------------------

17--------------------------------------------------------------------------------

@@ -29,6 +21,20 @@ interface DecEq t where

29 ||| Decide whether two elements of `t` are propositionally equal

21 ||| Decide whether two elements of `t` are propositionally equal

30 total decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)

22 total decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)

31

23

24+--------------------------------------------------------------------------------

25+-- Utility lemmas

26+--------------------------------------------------------------------------------

27+

28+||| The negation of equality is symmetric (follows from symmetry of equality)

29+total negEqSym : {a : t} -> {b : t} -> (a = b -> Void) -> (b = a -> Void)

30+negEqSym p h = p (sym h)

31+

32+||| Everything is decidably equal to itself

33+total decEqSelfIsYes : DecEq a => {x : a} -> decEq x x = Yes Refl

34+decEqSelfIsYes {x} with (decEq x x)

35+ | Yes Refl = Refl

36+ | No contra = absurd $ contra Refl

37+

32--------------------------------------------------------------------------------

38--------------------------------------------------------------------------------

33--- Unit

39--- Unit

34--------------------------------------------------------------------------------

40--------------------------------------------------------------------------------

libs/prelude/Prelude/Bool.idr+9

@@ -35,3 +35,12 @@ not : Bool -> Bool

35not True = False

36not False = True

37

38+--------------------------------------------------------------------------------

39+-- Properties

40+--------------------------------------------------------------------------------

41+

42+Uninhabited (True = False) where

43+ uninhabited Refl impossible

44+

45+Uninhabited (False = True) where

46+ uninhabited Refl impossible