@edwinbrady thanks for sharing the answer! so what would you use instead in practice?
I should add that I'm uncomfortable using 'so' there, but I think it's quicker to grasp for a casual reader than anything better (e.g. Dec)
-
-
-
@ma0e Instead of 'so' you mean? Depends, but often decidable equality (DecEq). 'Bool' is a bit of a code smell in a DT language, IMO. - 2 more replies
New conversation -
-
-
@edwinbrady Showing "so" isn't really fair as its use is so strongly discouraged. It's sending the reader down an attractive dead end. -
@a_cowley Teaching people the best way first, rather than the easiest way, is a good way to have them give up and dismiss it as too hard. - 4 more replies
New conversation -
-
-
@edwinbrady It almost reads as doge. Either (wow result) (wow (such result)) -
@acid2 I once suggested "data such : Bool -> Type where wow : such True"
End of conversation
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.