git.iko.soy/Idris-dev
on master help sign in
Remove superfluous clause in fact
d17224dMelvar Chen
libs/prelude/Prelude/Nat.idr−1
compare with master
unifiedsplit
@@ -223,7 +223,6 @@ fib (S (S n)) = fib (S n) + fib n
223
223
224total fact : Nat -> Nat
224total fact : Nat -> Nat
225fact Z = S Z
225fact Z = S Z
226−fact (S Z) = S Z
227fact (S n) = (S n) * fact n
226fact (S n) = (S n) * fact n
228
227
229--------------------------------------------------------------------------------
228--------------------------------------------------------------------------------