Boolean - Tumblr Posts

Hey so, Type Families and Propositional Type Equality in Haskell are pretty cool even if I mostly used them as hacks for Haskell not having dependent typing.

First time I've heavily used Data.Type.Equality.

Rewriting proofs with `trans` is significantly more tedious in compound types and results in quite a few functions to help guide the types.

Overall pretty fun experience. Lack of `rewrite` really does ruin a lot of the satisfaction though.

(I also made it into a Kata)

Codewars

Prove without Truth Tables

You are to prove the following equality: (p ∨ q) ⇒ r ≡ (p ⇒ r) ∧ (p ⇒ r) proof :: Bool p -> Bool q -> Bool r -> (p || q) ==>