git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' of github.com:idris-lang/Idris-dev
commite8596bc6e50725a4a312c8fbe7b1cd6fa6d2b4cf authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 20 Jul 2017, 22:06 (9 years ago) parentb6c0ae4a8a4564
8 files changed+43−21
compare with master
unifiedsplit
CHANGELOG.md+3 docs/reference/elaborator-reflection.rst+6−1 docs/reference/ide-protocol.rst+1−4 docs/reference/syntax-guide.rst+7−1 docs/tutorial/interfaces.rst+2−2 libs/contrib/Data/Heap.idr−4 libs/prelude/Decidable/Equality.idr+15−9 libs/prelude/Prelude/Bool.idr+9
CHANGELOG.md+3
@@ -22,6 +22,9 @@
2222 with a (strictly) smaller `size`.
2323
2424 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`.
2528
2629## Tool Updates
2730
docs/reference/elaborator-reflection.rst+6−1
@@ -32,6 +32,9 @@ Running Elaborator Scripts
3232
3333On their own, tactics have no effect.
3434The 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).
3538For example, the following script constructs the identity function at type ``Nat``:
3639
3740.. code-block:: idris
@@ -88,7 +91,9 @@ that fills the hole.
8891
8992The interactive elaboration shell accepts a limited number of commands,
9093including 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``.
9297
9398General-purpose commands:
9499
docs/reference/ide-protocol.rst+1−4
@@ -51,9 +51,6 @@ The available commands include:
5151 ``(:interpret STRING)``
5252 Interpret ``STRING`` at the Idris REPL, returning a highlighted result.
5353
54− ``(:repl-completions STRING)``
55− Return the result of tab-completing ``STRING`` as a REPL command.
56−
5754 ``(:type-of STRING)``
5855 Return the type of the name, written with Idris syntax in the ``STRING``.
5956 The reply may contain highlighting information.
@@ -122,7 +119,7 @@ The available commands include:
122119 Return the definition of ``NAME`` as a highlighted string.
123120
124121 ``(: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.
126123
127124 ``:version``
128125 Return the version information of the Idris compiler.
docs/reference/syntax-guide.rst+7−1
@@ -387,10 +387,16 @@ Totality
387387::
388388
389389 total
390− implicit
391390 partial
392391 covering
393392
393+Implicit Coercion
394+^^^^^^^^^^^^^^^^^
395+
396+::
397+
398+ implicit
399+
394400Options
395401^^^^^^^
396402
docs/tutorial/interfaces.rst+2−2
@@ -48,8 +48,8 @@ For example, the
4848Only one implementation of an interface can be given for a type — implementations may
4949not overlap. Implementation declarations can themselves have constraints.
5050To help with resolution, the arguments of an implementation must be
51−constructors (either data or type constructors), variables or
52−constants (i.e. you cannot give an implementation for a function). For
51+constructors (either data or type constructors) or variables
52+(i.e. you cannot give an implementation for a function). For
5353example, to define a ``Show`` implementation for vectors, we need to know
5454that there is a ``Show`` implementation for the element type, because we are
5555going 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
132132-- Properties
133133--------------------------------------------------------------------------------
134134
135−total
136−absurdBoolDischarge : False = True -> Void
137−absurdBoolDischarge Refl impossible
138−
139135total
140136isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = Z
141137isEmptySizeZero Empty p = Refl
libs/prelude/Decidable/Equality.idr+15−9
@@ -8,18 +8,10 @@ import Prelude.Either
88import Prelude.List
99import Prelude.Nat
1010import Prelude.Maybe
11+import Prelude.Uninhabited
1112
1213%access public export
1314
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−
2315--------------------------------------------------------------------------------
2416-- Decidable equality
2517--------------------------------------------------------------------------------
@@ -29,6 +21,20 @@ interface DecEq t where
2921 ||| Decide whether two elements of `t` are propositionally equal
3022 total decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
3123
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+
3238--------------------------------------------------------------------------------
3339--- Unit
3440--------------------------------------------------------------------------------
libs/prelude/Prelude/Bool.idr+9
@@ -35,3 +35,12 @@ not : Bool -> Bool
3535not True = False
3636not False = True
3737
38+--------------------------------------------------------------------------------
39+-- Properties
40+--------------------------------------------------------------------------------
41+
42+Uninhabited (True = False) where
43+ uninhabited Refl impossible
44+
45+Uninhabited (False = True) where
46+ uninhabited Refl impossible