git.iko.soy/Idris-dev
on master help sign in
Merge pull request #753 from Melvar/obstructive-fact-clause
ae56b06Edwin Brady
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--------------------------------------------------------------------------------