@idrislang has them, too: https://github.com/idris-lang/Idris-dev/commit/180fc75336577d329d7e03a05d81f9d74c8e6000 …https://twitter.com/andreasdotorg/status/879770150475636736 …
BTW: that thing where F* uses Z3 to dissolve boring proofs is definitely worth stealing for Idris.
-
-
Gotta love that syntax of Z3!
-
Wonder whether our in-house constraint solver people would like to have a stab at that...
-
@ozgurakgun and I thought about something like this a while ago... Probably worth doing something some day. -
I even drafted a fellowship application on the subject! Idris helping our tools, us helping Idris was the crux of idea...
-
That kind of thing never seems to be successful. Not shiny enough I guess.
-
eh, there's actually a fair amount of work on this kind of thing, and it's probably where theorem provers are going.
-
I should have been more specific: Any grant application I have been involved in that tried to marry two things to help each other failed.
-
I am starting to doubt the "killer application" argument, because I yet have to come across one that convinces the funders & reviewers.
- 1 more reply
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.