You can clone with
No one assigned
fact : Nat -> Nat
fact O = 1
fact (S n) = (S n) * fact n
choose : Nat -> Nat -> Nat
choose n k =
fact n `div` (fact k * fact (n - k))
pow : Nat -> Nat -> Nat
pow _ O = 1
pow x (S n) = x * pow x n
binomial : Nat -> Nat -> Nat -> Nat
binomial x y n =
sum $ map (\k => choose n k * (pow x (n - k)) * pow y k) [0..n]
binomialPrf : pow (x + y) n = binomial x y n
binomialPrf = believe_me ()
main : IO ()
main = print "hello world"
It just sits there using more and more memory attempting to typecheck this. It got up to almost 8GB before I remembered to ctrl-C.
The problem here is in writing the .ibc, not directly typechecking. And this is caused by the definition of [0..n], which expands indefinitely if n is not known, which it isn't in the type of binomialPrf.
[0..n] is implemented by the Prelude.count function which, as you'll see, is implemented using 'if' and is %assert_total, and this is probably not a good way to do it.
I've made 'count' partial, abstract and removed the '%assert_total' so that it won't reduce, so writing out the ibc now works. I'm not sure exactly what the issue is here though. Everything behaved as it was intended to, the problem was that an '%assert_total' function really shouldn't have been - that should be reserved for things which are safe to reduce at compile-time, which count isn't.
Make 'count' partial/abstract to prevent compile-time reduction
Deals with issue #171