These are chat archives for got-lambda/expression
The online hangout for Göteborg Functional Programming Group and everybody interested.
Is working code and a lost smarter than my example :p what you wrote is actually a proof, so much stronger than a unit test. My implementation was literally "if this value is False, crash compilation" for a bunch of Booleans :p
f : (5 = 3 + 2, 1 + 0 = 1) f = (Refl, Refl)