edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-24 04:43:25 +03:00
Code Issues Projects Releases Wiki Activity

Update updates.rst

Browse Source
This commit is contained in:
GhiOm 2020-02-27 12:51:11 +01:00 committed by GitHub
parent 52e6a4f1ed
commit 37af02eb2a
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
docs/updates/updates.rst
View File

@ -554,7 +554,7 @@ field:
constructor MkVect constructor MkVect
purpose : String purpose : String
length : Nat length : Nat
content : Vect len a content : Vect length a
Then, we can safely update the ``content``, provided we update the ``length`` Then, we can safely update the ``content``, provided we update the ``length``
correspondingly: correspondingly:
@ -562,7 +562,7 @@ correspondingly:
.. code-block:: idris .. code-block:: idris
addEntry : String -> WrapVect String -> WrapVect String addEntry : String -> WrapVect String -> WrapVect String
addEntry val = record { len $= S, addEntry val = record { length $= S,
content $= (val :: ) } content $= (val :: ) }
Generate definition Generate definition