File tree Expand file tree Collapse file tree 1 file changed +5
-5
lines changed Expand file tree Collapse file tree 1 file changed +5
-5
lines changed Original file line number Diff line number Diff line change @@ -359,9 +359,9 @@ For example, the type of \idr{negb True} is \idr{Bool}.
359
359
360
360
```idris
361
361
λΠ> :type True
362
- -- True : Bool
362
+ True : Bool
363
363
λΠ> :t negb True
364
- -- negb True : Bool
364
+ negb True : Bool
365
365
```
366
366
367
367
\todo[inline]{Confirm the "function types " wording.}
@@ -372,7 +372,7 @@ with arrows.
372
372
373
373
```idris
374
374
λΠ> :t negb
375
- -- negb : Bool -> Bool
375
+ negb : Bool -> Bool
376
376
```
377
377
378
378
The type of \idr{negb}, written \idr{Bool -> Bool} and pronounced "\idr{Bool}
@@ -458,9 +458,9 @@ default:
458
458
459
459
```idris
460
460
λΠ> S (S (S (S Z )))
461
- -- 4 : Nat
461
+ 4 : Nat
462
462
λΠ> minusTwo 4
463
- -- 2 : Nat
463
+ 2 : Nat
464
464
```
465
465
466
466
The constructor \idr{S} has the type \idr{Nat -> Nat}, just like the functions
You can’t perform that action at this time.
0 commit comments