Still plenty to do, but it's probably more likely to happen if I let other people have a go :). I've got as far as Chapter 11 of the TypeDD book in updating examples, so at least there's some evidence that things are starting to work...
-
-
Show this threadThanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
Does this mean I can have good runtime monitoring by optionally retaining type information? If so I'm giddy with excitement.pic.twitter.com/jADSdSlQTw
-
Types can hang around at run time if you want, if that's what you mean, yes. Here's a tiny example: https://github.com/edwinb/Idris2/blob/master/tests/chez/chez007/TypeCase.idr …
End of conversation
New conversation -
-
-
do you need any help ? im new to DT but would like to contribute as im planning to write msc thesis on DT.
-
Yes please! There's loads needs doing. See https://github.com/edwinb/Idris2/blob/master/CONTRIBUTING.md … for a few ideas
End of conversation
New conversation -
-
-
Can we hope for laziness by default?
-
You can hope for anything you like! There's a fork button on github, and Idris makes it easy to write new backends, which will continue.
End of conversation
New conversation -
-
-
I know the first one was named after the dragon but surely *this* one named after Idris Elba
-
Actually, this one's named after the last king of Libya, Idris Senussi.
- 3 more replies
New conversation -
-
-
U r a wonderful human being.
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
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.