Copyright | (c) Levent Erkok |
---|---|
License | BSD3 |
Maintainer | erkokl@gmail.com |
Stability | experimental |
Safe Haskell | None |
Language | Haskell2010 |
A puzzle, attributed to Lewis Caroll:
- All rabbits, that are not greedy, are black
- No old rabbits are free from greediness
- Therefore: Some black rabbits are not old
What's implicit here is that there is a rabbit that must be not-greedy; which we add to our constraints.
Documentation
A universe of rabbits
Instances
greedy :: SRabbit -> SBool Source #
Identify those rabbits that are greedy. Note that we leave the predicate uninterpreted.
black :: SRabbit -> SBool Source #
Identify those rabbits that are black. Note that we leave the predicate uninterpreted.
old :: SRabbit -> SBool Source #
Identify those rabbits that are old. Note that we leave the predicate uninterpreted.
rabbitsAreOK :: IO ThmResult Source #
Prove the claim. We have:
>>>
rabbitsAreOK
Q.E.D.