Skip to content

Commit 5e019b7

Browse files
authored
removed extra parenthesis (#90)
1 parent 7e3f55d commit 5e019b7

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

src/Tutorial/Dependent.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@ Before we proceed to our example, first consider how Idris recursively
4040
defines the natural numbers (here affixed with apostrophes to avoid introducing
4141
a conflict with the actual definition of `Nat`, which you can find
4242
[here](https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Prelude/Nat.idr)
43-
for reference)):
43+
for reference):
4444

4545
```idris
4646
data Nat' : Type where

0 commit comments

Comments
 (0)