Edwin Brady

**Comment by [edwinb](https://github.com/edwinb)** _Thursday May 07, 2020 at 11:34 GMT_ ---- Diamond shaped inheritance structures are awkward because implementations of the same interface aren't guaranteed to be equal. There's a...

**Comment by [nickdrozd](https://github.com/nickdrozd)** _Thursday May 07, 2020 at 14:02 GMT_ ---- I'm pretty sure this is what's responsible for blocking the proof at https://github.com/idris-lang/Idris-dev/pull/4848/files#diff-fb2a7c0a9ce133762a38755823a01d7aR73. > By the way, I don't...

**Comment by [nickdrozd](https://github.com/nickdrozd)** _Thursday May 07, 2020 at 14:05 GMT_ ---- This change does not fix the issue, or even affect the error message: ```diff -interface (VerifiedSemigroup a, Monoid a)...

**Comment by [faserprodukt](https://github.com/faserprodukt)** _Friday May 08, 2020 at 01:09 GMT_ ---- > So, this code as it stands isn't going to work without some modification. This diamond issue is a...

**Comment by [Sventimir](https://github.com/Sventimir)** _Thursday May 14, 2020 at 17:45 GMT_ ---- > By the way, I don't think we should use the names `VerifiedX` any more - having the repeated...

This shouldn't be necessary - I'll look into it. Plenty of tests should have caught this, so it's a bit mysterious...

Oops, yes, found the problem (but not the solution yet...). Hopefully it'll be a quick fix!

I've made a change to master to deal with function parameters properly, so this should be unnecessary now... On 8 Aug 2014, at 05:52, stepcut [email protected] wrote: > This patch...

**Comment by [edwinb](https://github.com/edwinb)** _Friday Mar 27, 2020 at 20:51 GMT_ ---- The strange behaviour is probably because in `TestStruct`, `ExtraStruct` isn't a pointer. A `Struct` on the Idris side needs...

One thing I've wanted in the past is the ability to pick a definition according to the code generator in use. I've never worked out the details though. One difficulty...