Skip to content

Commit

Permalink
Merge pull request #3255 from foxyseta/patch-1
Browse files Browse the repository at this point in the history
doc: typos in "Types and Functions"
  • Loading branch information
andrevidela committed Apr 12, 2024
2 parents b690dc1 + 12c4a94 commit 4799d28
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions docs/source/tutorial/typesfuns.rst
Original file line number Diff line number Diff line change
Expand Up @@ -794,7 +794,7 @@ their type. As syntactic sugar, any implementation of the names
Similarly, any implementation of the names ``Lin`` and ``:<`` can be
written in **snoc**-list form:

- ``[<]`` mean ``Lin``
- ``[<]`` means ``Lin``
- ``[< 1, 2, 3]`` means ``Lin :< 1 :< 2 :< 3``.

and the prelude includes a pre-defined datatype for snoc-lists:
Expand Down Expand Up @@ -1388,7 +1388,7 @@ Idris distinguishes between *total* and *partial* functions.
A total function is a function that either:
+ Terminates for all possible inputs, or
+ Produces a non-empty, finite, prefix of a possibly infinite result
+ Produces a non-empty, finite prefix of a possibly infinite result
If a function is total, we can consider its type a precise description of what
that function will do. For example, if we have a function with a return
Expand Down

0 comments on commit 4799d28

Please sign in to comment.