Mastodon Feed: Post

dysfun@treehouse.systems ("gaytabase") wrote:

i just worked out how to get custom typecheck error messages in idris.

first of all, you need an implicit argument to a proof of some property. you set the default to call a function which returns a proof of the appropriate type.

at any point if something is wrong, that function uses idris_crash to show a helpful error message.