Joel Berkeley
Joel Berkeley
Hi, yes I am maximising my screen, and that's very much my preferred style. I would have thought that was how most people use browsers.
It continues, with ``` symmetric : (s, s' : String) -> s == s' = s' == s symmetric s s' with (s == s') proof e | (s' ==...
I've implemented `symmetric` another way. The bug remains, however
I'd have thought top level functions with quantity `1` should only be possible if private, and used exactly once in the module (though I can't imagine why you'd want one)....
I think this means that a top-level linear object can only be used within the same module as a non-exported `main` function.
Hi. I don't feel this concern on its own warrants rethinking the interface mechanism. But to reply to your point: I don't recall if nested functions are compiled to the...
yes, I'd forgotten about that. I feel some kind of documentation or error message is the most likely solution
BTW this wasn't a problem for me. I knew how to fix it, but made this ticket as it seemed like something newcomers might get confused by.
Note, given the state we're in now, can we just make `tag` use linearity, which will mean most computations won't require linearity, and it will drop the `Tag` monad entirely.
can we make everything linear, but overload `fromDouble` etc. as an unrestricted tensor, on the basis that calculations on scalars aren't likely to be a bottleneck? Users wouldn't be able...