I've been teaching the Idris program synthesis gadget to not give up after the first result. This is where we're up to... https://gist.github.com/edwinb/9b5dfda2ddf402133ab5d2ce47e85f3e
Just hacked this into the vim mode. Imagine I'm hitting the type declaration with a hammer between each implementation.
It's interesting to see where it goes if you make the lists linear. The first answer is the right one here...
In other news, TIL you can record and edit your screen in Linux. What is this sorcery!
Thanks to a suggestion by @Augustsson (generate some candidates then sort by fraction of bound variables used) it gets the right answer much quicker now.
@edwinb Wow *_*
@raichoo This is fun, although I don't know if it's going to work for anything real until the program synthesis is improved some more!
@edwinb Seems to be a pretty interesting place for exploration though ^^. Looking forward to what you are going to build there 😸
@edwinb how did you record and edit your screen in Linux?
@shapr I recorded with kazam then cropped with HandBrake.
One annoying challenge is that lots of programs don't cope well with HiDPI (kazam didn't, I had to put the window in the right corner of the screen!)
Server run by the main developers of the project It is not focused on any particular niche interest - everyone is welcome as long as you follow our code of conduct!