search

idris-hackers / software-foundations

Software Foundations in Idris
https://idris-hackers.github.io/software-foundations
MIT License
452 stars 34 forks source link

Page 18, mult function is wrong #59

Open PhilAndrew opened 5 years ago

PhilAndrew commented 5 years ago

Idris version 1.3.2

mult : (n, m : Nat) -> Nat
mult Z = Z
mult (S k) = plus m (mult k m)

Should be

mult : (n, m : Nat) -> Nat
mult Z _ = Z
mult (S k) m = plus m (mult k m)
yurrriq commented 5 years ago

Thanks for catching this. Could you please submit a PR and mention me?

yurrriq commented 5 years ago

hmm.. looks like the .lidr is correct, right? I'll work on getting the build env up to date and rebuilding the PDF.