That’s very interesting, and looks a bit similar to the work I did on an applicative for proof search in TyDe 2016 http://liamoc.net/images/applications.pdf …
The new Agda standard library comes with my changes to `Dec` (known from an AIM wrap-up meeting and my SPLS talk). There's also a new wee bit of documentation at https://agda.github.io/agda-stdlib/README.Decidability.html …. It's aimed towards people new to `Dec`, but is hopefully useful for everyone.
-
-
-
Can you elaborate on why the changes to Dec were needed?
- Još 3 druga odgovora
Novi razgovor -
-
-
-
Cool! I remember trying a classic Dec proof in Haskell in preparation for my talk, but I didn't feel up to anything this adventurous. Do `map` and its computational properties work out the same in Haskell?
- Još 4 druga odgovora
Novi razgovor -
-
-
Are the SPLS slides available somewhere? Thanks.
-
Slides
? Here's a slightly presented version of the buffer I was working in:https://github.com/laMudri/bool-in-hand/blob/master/src/TalkExtra.agda … - Još 6 drugih odgovora
Novi razgovor -
Čini se da učitavanje traje već neko vrijeme.
Twitter je možda preopterećen ili ima kratkotrajnih poteškoća u radu. Pokušajte ponovno ili potražite dodatne informacije u odjeljku Status Twittera.