From 29a6aa45e02a044cf8a4f5e0dd777c76e7227505 Mon Sep 17 00:00:00 2001 From: stefan-hoeck Date: Fri, 22 Jan 2021 14:30:42 +0100 Subject: [PATCH] fixed whitespace for *.md and .rst files --- CONTRIBUTING.md | 2 +- INSTALL.md | 2 +- docs/source/app/exceptionsstate.rst | 2 -- docs/source/app/index.rst | 1 - docs/source/app/interfaces.rst | 2 -- docs/source/app/introapp.rst | 1 - docs/source/backends/custom.rst | 2 +- docs/source/backends/refc.rst | 2 +- docs/source/implementation/overview.rst | 2 +- docs/source/proofs/definitional.rst | 2 +- docs/source/proofs/index.rst | 2 +- docs/source/proofs/patterns.rst | 6 ++-- docs/source/proofs/propositional.rst | 7 ++-- docs/source/tutorial/conclusions.rst | 4 +-- docs/source/tutorial/interactive.rst | 1 - docs/source/tutorial/modules.rst | 14 ++++---- docs/source/tutorial/multiplicities.rst | 44 ++++++++++++------------- docs/source/tutorial/starting.rst | 2 +- 18 files changed, 44 insertions(+), 54 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 6e9dd802a..5ab655828 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -15,7 +15,7 @@ beyond work on the language core, are (in no particular order): - code colouring - it'd be nice if Ctrl-C didn't quit the whole system! * IDE mode improvements - - Syntax highlighting support for output + - Syntax highlighting support for output - Several functions from the version 1 IDE protocol are not yet implemented, and I haven't confirmed it works in everything. - (Not really part of Idris 2, but an editing mode for vim would be lovely!) diff --git a/INSTALL.md b/INSTALL.md index 1fa3d4641..233529a80 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -120,7 +120,7 @@ If you are a [nix](https://nixos.org/features.html) user you can install Idris 2 by running the following command: nix-env -i idris2 - + ### Install from nix flakes If you are a [nix flakes](https://nixos.wiki/wiki/Flakes) user you can install Idris 2 together with all the requirements by running the following command: diff --git a/docs/source/app/exceptionsstate.rst b/docs/source/app/exceptionsstate.rst index 30e770490..e06970fd9 100644 --- a/docs/source/app/exceptionsstate.rst +++ b/docs/source/app/exceptionsstate.rst @@ -85,5 +85,3 @@ Rather than using ``State`` and ``Exception`` directly, however, we typically use interfaces to constrain the operations which are allowed in a list of errors. Internally, ``State`` is implemented via an ``IORef``, primarily for performance reasons. - - diff --git a/docs/source/app/index.rst b/docs/source/app/index.rst index f24b8765d..cf6478916 100644 --- a/docs/source/app/index.rst +++ b/docs/source/app/index.rst @@ -53,4 +53,3 @@ interfaces. exceptionsstate interfaces linear - diff --git a/docs/source/app/interfaces.rst b/docs/source/app/interfaces.rst index 6cf834dc0..11d6b9a9e 100644 --- a/docs/source/app/interfaces.rst +++ b/docs/source/app/interfaces.rst @@ -144,5 +144,3 @@ with any errors thrown by ``readFile``: readMain fname = handle (readFile fname) (\str => putStrLn $ "Success:\n" ++ show str) (\err : IOError => putStrLn $ "Error: " ++ show err) - - diff --git a/docs/source/app/introapp.rst b/docs/source/app/introapp.rst index 585e9e604..de756efa3 100644 --- a/docs/source/app/introapp.rst +++ b/docs/source/app/introapp.rst @@ -105,4 +105,3 @@ is ``NoThrow`` or ``MayThrow``. But, in practice, all applications given to ``run`` will not throw at the top level, because the only exception type available is the empty type ``Void``. Any exceptions will have been introduced and handled inside the ``App``. - diff --git a/docs/source/backends/custom.rst b/docs/source/backends/custom.rst index b250ceca2..8e4d7d687 100644 --- a/docs/source/backends/custom.rst +++ b/docs/source/backends/custom.rst @@ -5,7 +5,7 @@ Building Idris 2 with new backends The way to extend Idris 2 with new backends is to use it as a library. The module ``Idris.Driver`` exports the function ``mainWithCodegens``, that takes a list of ``(String, Codegen)``, -starting idris with these codegens in addition to the built-in ones. The first +starting idris with these codegens in addition to the built-in ones. The first codegen in the list will be set as the default codegen. Getting started diff --git a/docs/source/backends/refc.rst b/docs/source/backends/refc.rst index eb10d5765..9256b4abf 100644 --- a/docs/source/backends/refc.rst +++ b/docs/source/backends/refc.rst @@ -6,7 +6,7 @@ There is an experimental code generator which compiles to an executable via C, using a reference counting garbage collector. This is intended as a lightweight (i.e. minimal dependencies) code generator that can be ported to multiple platforms, especially those with memory constraints. - + Performance is not as good as the Scheme based code generators, partly because the reference counting has not yet had any optimisation, and partly because of the limitations of C. However, the main goal is portability: the generated diff --git a/docs/source/implementation/overview.rst b/docs/source/implementation/overview.rst index f5f05d3ed..640aa0efa 100644 --- a/docs/source/implementation/overview.rst +++ b/docs/source/implementation/overview.rst @@ -44,7 +44,7 @@ Where to find things: * ``Core/`` -- anything related to the core TT, typechecking and unification * ``TTImp/`` -- anything related to the implicit TT and its elaboration - + ``TTImp/Elab/`` -- Elaboration state and elaboration of terms + + ``TTImp/Elab/`` -- Elaboration state and elaboration of terms + ``TTImp/Interactive/`` -- Interactive editing infrastructure * ``Parser/`` -- various utilities for parsing and lexing TT and TTImp (and other things) diff --git a/docs/source/proofs/definitional.rst b/docs/source/proofs/definitional.rst index f1229ee25..b0fa114da 100644 --- a/docs/source/proofs/definitional.rst +++ b/docs/source/proofs/definitional.rst @@ -31,7 +31,7 @@ Or if the ``proposition`` is, +-------+ we can't prove it is true, but it is still a valid proposition and perhaps we -can prove it is false so the ``judgment`` is, +can prove it is false so the ``judgment`` is, +-------------+ | 1+1=3 false | diff --git a/docs/source/proofs/index.rst b/docs/source/proofs/index.rst index 904c524c3..797be86bd 100644 --- a/docs/source/proofs/index.rst +++ b/docs/source/proofs/index.rst @@ -4,7 +4,7 @@ Theorem Proving ############### -A tutorial on theorem proving in Idris 2. +A tutorial on theorem proving in Idris 2. .. note:: diff --git a/docs/source/proofs/patterns.rst b/docs/source/proofs/patterns.rst index bc18f334d..ed621e00b 100644 --- a/docs/source/proofs/patterns.rst +++ b/docs/source/proofs/patterns.rst @@ -101,7 +101,7 @@ yields: plus_commutes (S k) m = ?plus_commutes_S That is, the hole has been filled with a call to a top level -function ``plus_commutes_Z``, applied to the variable in scope ``m``. +function ``plus_commutes_Z``, applied to the variable in scope ``m``. Unfortunately, we cannot prove this lemma directly, since ``plus`` is defined by matching on its *first* argument, and here ``plus m Z`` has a @@ -113,14 +113,14 @@ First, create a template definition with ``\d``: .. code-block:: idris - plus_commutes_Z : (m : Nat) -> m = plus m Z + plus_commutes_Z : (m : Nat) -> m = plus m Z plus_commutes_Z m = ?plus_commutes_Z_rhs Now, case split on ``m`` with ``\c``: .. code-block:: idris - plus_commutes_Z : (m : Nat) -> m = plus m Z + plus_commutes_Z : (m : Nat) -> m = plus m Z plus_commutes_Z Z = ?plus_commutes_Z_rhs_1 plus_commutes_Z (S k) = ?plus_commutes_Z_rhs_2 diff --git a/docs/source/proofs/propositional.rst b/docs/source/proofs/propositional.rst index 0159b242b..2ea2fe0c6 100644 --- a/docs/source/proofs/propositional.rst +++ b/docs/source/proofs/propositional.rst @@ -26,7 +26,7 @@ match all possible values of ``n``. In this case plusReducesR : (n : Nat) -> plus n Z = n plusReducesR Z = Refl - plusReducesR (S k) + plusReducesR (S k) = let rec = plusReducesR k in rewrite sym rec in Refl @@ -118,7 +118,7 @@ and these are also included in the prelude: Heterogeneous Equality ====================== -Also included in the prelude: +Also included in the prelude: .. code-block:: idris @@ -130,6 +130,3 @@ Also included in the prelude: ||| @ y the right side (~=~) : (x : a) -> (y : b) -> Type (~=~) x y = (x = y) - - - diff --git a/docs/source/tutorial/conclusions.rst b/docs/source/tutorial/conclusions.rst index 4d60f022d..b01047d06 100644 --- a/docs/source/tutorial/conclusions.rst +++ b/docs/source/tutorial/conclusions.rst @@ -25,11 +25,11 @@ dependent types in general, can be obtained from various sources: * Examining the prelude and exploring the ``samples`` in the distribution. The Idris 2 source can be found online at: - + * https://github.com/edwinb/Idris2. * Existing projects on the ``Idris Hackers`` web space: - + * https://idris-hackers.github.io. * Various papers (e.g. [#BradyHammond2012]_, [#Brady]_, and [#BradyHammond2010]_). Although these mostly diff --git a/docs/source/tutorial/interactive.rst b/docs/source/tutorial/interactive.rst index a63fa8f7a..cfb9528dc 100644 --- a/docs/source/tutorial/interactive.rst +++ b/docs/source/tutorial/interactive.rst @@ -261,4 +261,3 @@ by using ``idris2 -–client``. More sophisticated support can be added by using the IDE protocol (yet to be documented for Idris 2, but which mostly extends to protocol documented for `Idris 1 `_. - diff --git a/docs/source/tutorial/modules.rst b/docs/source/tutorial/modules.rst index 34b69bdea..f84115bb6 100644 --- a/docs/source/tutorial/modules.rst +++ b/docs/source/tutorial/modules.rst @@ -117,7 +117,7 @@ Meaning for Functions about doing this. .. note:: - + Type synonyms in Idris are created by writing a function. When setting the visibility for a module, it is usually a good idea to ``public export`` all type synonyms if they are to be used outside @@ -130,15 +130,15 @@ Therefore, it's generally a good idea to avoid using ``public export`` for functions unless you really mean to export the full definition. .. note:: - *For beginners*: + *For beginners*: If the function needs to be accessed only at runtime, use ``export``. - However, if it's also meant to be used at *compile* time (e.g. to prove - a theorem), use ``public export``. + However, if it's also meant to be used at *compile* time (e.g. to prove + a theorem), use ``public export``. For example, consider the function ``plus : Nat -> Nat -> Nat`` discussed - previously, and the following theorem: ``thm : plus Z m = m``. - In order to to prove it, the type checker needs to reduce ``plus Z m`` to ``m`` + previously, and the following theorem: ``thm : plus Z m = m``. + In order to to prove it, the type checker needs to reduce ``plus Z m`` to ``m`` (and hence obtain ``thm : m = m``). - To achieve this, it will need access to the *definition* of ``plus``, + To achieve this, it will need access to the *definition* of ``plus``, which includes the equation ``plus Z m = m``. Therefore, in this case, ``plus`` has to be marked as ``public export``. diff --git a/docs/source/tutorial/multiplicities.rst b/docs/source/tutorial/multiplicities.rst index 7ef0dfa5d..09e0289c4 100644 --- a/docs/source/tutorial/multiplicities.rst +++ b/docs/source/tutorial/multiplicities.rst @@ -76,7 +76,7 @@ By "used" we mean either: * if the variable is a data type or primitive value, it is pattern matched against, ex. by being the subject of a *case* statement, or a function argument that is pattern matched against, etc., * if the variable is a function, that function is applied (i.e. ran with an argument) - + First, we'll see how this works on some small examples of functions and data types, then see how it can be used to encode `resource protocols`_. @@ -151,10 +151,10 @@ wraps an argument with unrestricted use data Lin : Type -> Type where MkLin : (1 _ : a) -> Lin a - + data Unr : Type -> Type where MkUnr : a -> Unr a - + If ``MkLin x`` is used once, then ``x`` is used once. But if ``MkUnr x`` is used once, there is no guarantee on how often ``x`` is used. We can see this a bit more clearly by starting to write projection functions for ``Lin`` and @@ -164,10 +164,10 @@ bit more clearly by starting to write projection functions for ``Lin`` and getLin : (1 _ : Lin a) -> a getLin (MkLin x) = ?howmanyLin - + getUnr : (1 _ : Unr a) -> a getUnr (MkUnr x) = ?howmanyUnr - + Checking the types of the holes shows us that, for ``getLin``, we must use ``x`` exactly once (Because the ``val`` argument is used once, by pattern matching on it as ``MkLin x``, and if ``MkLin x`` is used once, @@ -197,7 +197,7 @@ If ``getLin`` has an unrestricted argument... getLin (MkLin x) = ?howmanyLin ...then ``x`` is unrestricted in ``howmanyLin``:: - + Main> :t howmanyLin 0 a : Type x : a @@ -267,12 +267,12 @@ So an example correct door protocol usage would be .. code-block:: idris doorProg : IO () - doorProg + doorProg = newDoor $ \d => let d' = openDoor d d'' = closeDoor d' in deleteDoor d'' - + It's instructive to build this program interactively, with holes along the way, and see how the multiplicities of ``d``, ``d'`` etc change. For example @@ -280,7 +280,7 @@ example .. code-block:: idris doorProg : IO () - doorProg + doorProg = newDoor $ \d => let d' = openDoor d in ?whatnow @@ -302,7 +302,7 @@ It's also fine to shadow the name ``d`` throughout .. code-block:: idris doorProg : IO () - doorProg + doorProg = newDoor $ \d => let d = openDoor d d = closeDoor d in @@ -315,7 +315,7 @@ can try not to delete the door before finishing .. code-block:: idris doorProg : IO () - doorProg + doorProg = newDoor $ \d => let d' = openDoor d d'' = closeDoor d' in @@ -332,7 +332,7 @@ at the type level. If we have an external resource which is guaranteed to be used linearly, like ``Door``, we don't need to run operations on that resource in an ``IO`` monad, since we're already enforcing an ordering on operations and don't have access to any out of date resource states. This is -similar to the way interactive programs work in +similar to the way interactive programs work in `the Clean programming language `_, and in fact is how ``IO`` is implemented internally in Idris 2, with a special ``%World`` type for representing the state of the outside world that is @@ -380,7 +380,7 @@ For example, in Idris 1 you could get the length of a vector as follows vlen : Vect n a -> Nat vlen {n} xs = n - + This is fine, since it runs in constant time, but the trade off is that ``n`` has to be available at run time, so at run time we always need the length of the vector to be available if we ever call ``vlen``. Idris 1 can infer whether @@ -392,7 +392,7 @@ In Idris 2, we need to state explicitly that ``n`` is needed at run time vlen : {n : Nat} -> Vect n a -> Nat vlen xs = n - + (Incidentally, also note that in Idris 2, names bound in types are also available in the definition without explicitly rebinding them.) @@ -403,12 +403,12 @@ example, this will give an error sumLengths : Vect m a -> Vect n a —> Nat sumLengths xs ys = vlen xs + vlen ys - + Idris 2 reports:: vlen.idr:7:20--7:28:While processing right hand side of Main.sumLengths at vlen.idr:7:1--10:1: m is not accessible in this context - + This means that it needs to use ``m`` as an argument to pass to ``vlen xs``, where it needs to be available at run time, but ``m`` is not available in ``sumLengths`` because it has multiplicity ``0``. @@ -420,7 +420,7 @@ We can see this more clearly by replacing the right hand side of sumLengths : Vect m a -> Vect n a -> Nat sumLengths xs ys = ?sumLengths_rhs - + ...then checking the hole's type at the REPL:: Main> :t sumLengths_rhs @@ -450,7 +450,7 @@ though, that if you have bound implicits, such as... .. code-block:: idris excitingFn : {t : _} -> Coffee t -> Moonbase t - + ...then it's a good idea to make sure ``t`` really is needed, or performance might suffer due to the run time building the instance of ``t`` unnecessarily! @@ -466,7 +466,7 @@ elsewhere. So, the following definition is rejected This is rejected with the error:: - badnot.idr:2:1--3:1:Attempt to match on erased argument False in + badnot.idr:2:1--3:1:Attempt to match on erased argument False in Main.badNot The following, however, is fine, because in ``sNot``, even though we appear @@ -478,7 +478,7 @@ the type of the second argument data SBool : Bool -> Type where SFalse : SBool False STrue : SBool True - + sNot : (0 x : Bool) -> SBool x -> Bool sNot False SFalse = True sNot True STrue = False @@ -495,13 +495,13 @@ Pattern Matching on Types ------------------------- One way to think about dependent types is to think of them as "first class" -objects in the language, in that they can be assigned to variables, +objects in the language, in that they can be assigned to variables, passed around and returned from functions, just like any other construct. But, if they're truly first class, we should be able to pattern match on them too! Idris 2 allows us to do this. For example .. code-block:: idris - + showType : Type -> String showType Int = "Int" showType (List a) = "List of " ++ showType a diff --git a/docs/source/tutorial/starting.rst b/docs/source/tutorial/starting.rst index 2893537a3..6cf7fe5e5 100644 --- a/docs/source/tutorial/starting.rst +++ b/docs/source/tutorial/starting.rst @@ -89,7 +89,7 @@ which you can run: $ idris2 hello.idr -o hello $ ./build/exec/hello Hello world - + (On Macos you may first need to install realpath: ```brew install coreutils```) Please note that the dollar sign ``$`` indicates the shell prompt!