idris-lang/idris-tutorial — pull request #48 by gavlegoat (2014-11-04 17:58:54+00:00)
Title: Added the choose function to the So data type section

The tutorial mentions the So datatype as a way to ensure certain runtime tests have been performed but doesn't actually tell the reader how to construct a value of type So (how to convince the type checker that this runtime check has been made). This resolves #40 which I opened a while about about this problem.