André Videla
André Videla
@buzden I'm not sure what you are replying to but I think I can bring in some intuition about what is happening with erased quantities. Especially your statement > bringing...
Sorry for the late reply, in my experience with QTT and different semantics for quantity semirings there is a clear distinction between staging semantics and use semantics. It is true...
Software's not about blame! Don't feel pressure to mess up something.
I think @CodingCellist has a dot library we could use for that
oh boy I was waiting for this to happen, exciting
Any progress @freddi301 ?
I couldn't find instructions on how to run the tests locally so I hoped that CI would pick up the job but that does not seem to be the case,...
Maybe an easier way to deal with this would be to communicate where the term is stuck: ``` Bar> :reload 2/2: Building Bar (Bar.idr) Error: While processing right hand side...
In my opinion the most appropriate way to address this is with tree separate proposals: - implement the binding arrow `->` as its own fixity (with precedence -1) + operator...
Some personal notes: - Last year @stefan-hoeck showed us a very efficient constant-time parser using his library [idris2-parser](http://github.com/stefan-hoeck/idris2-parser). My personal assessment was that it's essentially the target to hit in...