Skip to content

Commit 048d033

Browse files
authored
Adds missing arguments to Playground2.mult
1 parent 41b6038 commit 048d033

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/Basics.lidr

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -550,8 +550,8 @@ just the same as if we had written \idr{(n : Nat) -> (m : Nat)}.
550550

551551
```idris
552552
mult : (n, m : Nat) -> Nat
553-
mult Z = Z
554-
mult (S k) = plus m (mult k m)
553+
mult Z _ = Z
554+
mult (S k) m = plus m (mult k m)
555555
```
556556

557557
> testMult1 : (mult 3 3) = 9

0 commit comments

Comments
 (0)