A classic pitfall of writing any kind of elaborator is that information you hold in your hand is invalidated by constraints that you've solved since you grabbed hold of it. Definition, not substitution is the key to not getting bitten. But then you have to remember to update.
-
Show this thread
-
Replying to @pigworker
I've been making this mistake occasionally for Idris 2, despite being aware of the pitfall. Idris 3 will make it harder to make it. By Idris 1000001 maybe I'll get the hang of it. But there's only so many Smallfilms characters.
1 reply 0 retweets 6 likes -
Replying to @edwinbrady
Knowing the problem's name is the first step to solving it. Is there a Smallfilms character particularly prone to loss of short term memory?
2 replies 0 retweets 0 likes -
Replying to @edwinbrady @pigworker
Also if I retire without having called something Yaffle something will have gone badly wrong.
3:12 PM - 1 Oct 2018
0 replies
0 retweets
2 likes
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.