search

edwinb / Idris2-boot

A dependently typed programming language, a successor to Idris
https://idris-lang.org/
Other
902 stars 58 forks source link

WIP: Bugfix named interfaces #296

Closed fabianhjr closed 4 years ago

fabianhjr commented 4 years ago

Closes #291

There seemed to be an issue of what was expected of interface implementations, in particular name appears to be a grammar for symbols/operators and not of identifiers.

Additionally something is off with the elaborator but I haven't been able to pin what.

edwinb commented 4 years ago

A name could be a symbol or operator, and although it would be a strange thing to do, it is therefore valid for a named implementation to be an operator. So the issue here isn't in the parsing, but rather in when the elaborator adds the named implementations to the searchable set. I have a fix for the issue, which I'll push shortly, so I'm going to close this PR.