Merge pull request #753 from Melvar/obstructive-fact-clause
Remove superfluous clause in fact
commitae56b0625f6e9639d6b7fd2c48d4dd5c81208699
authorEdwin Brady <edwin.brady@gmail.com>
dateMon 30 Dec 2013, 06:28 (13 years ago)
parent0a6fb1fd17224d
libs/prelude/Prelude/Nat.idr−1
@@ -223,7 +223,6 @@ fib (S (S n)) = fib (S n) + fib n
223223
224224total fact : Nat -> Nat
225225fact Z = S Z
226−fact (S Z) = S Z
227226fact (S n) = (S n) * fact n
228227
229228--------------------------------------------------------------------------------