bad-tests.disco

||| A function that doesn't do what it's supposed to.

!!! badmap (\x. x/0) [3,4,5] == [6,7,8]
!!! badmap (\x. x) [1,2] == [1,2]
!!! badmap (\x. x + 1) [3,4] > [5,6]

badmap : (Q -> Q) -> List(Q) -> List(Q)
badmap _ [] = [3]
badmap f (x::xs) = f x :: f x :: badmap f xs


||| A function we have some mistaken beliefs about.

!!! forall a : Q, b : Q. divide a b * b == a

!!! forall a : Q. divide a 2 < a

!!! exists a : Q. divide a 2 == abs a + 1

divide : Q -> Q -> Q
divide a b = a / b