Idris2/tests/idris2/linear007/expected

1/1: Building LCase (LCase.idr)
Error: While processing right hand side of foo. There are 0 uses of linear name y. 

LCase:11:11--13:41
 11 |     = let 1 test = the MyNat $ case z of
 12 |                         MyZ => MyZ
 13 |                         (MyS k) => MyS z

Suggestion: linearly bounded variables must be used exactly once.
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here! 2020-05-19 20:25:18 +03:00			`1/1: Building LCase (LCase.idr)`
Implementations and errors - Added initial implementations for terms and values - Error messages converted to pretty printer - Colorization for error messages - Color and console width option both as command line and repl command 2020-07-28 15:11:42 +03:00			`Error: While processing right hand side of foo. There are 0 uses of linear name y.`

[ new ] `--install-with-src`; refactoring around `FC`s (#1450) Why: * To implement robust cross-project go-to-definition in LSP i.e you can jump to definition of any global name coming from library dependencies, as well as from the local project files. What it does: * Modify `FC`s to carry `ModuleIdent` for .idr sources, file name for .ipkg sources or nothing for interactive runs. * Add `--install-with-src` to install the source code alongside the ttc binaries. The source is installed into the same directory as the corresponding ttc file. Installed sources are made read-only. * As we install the sources pinned to the related ttc files we gain the versioning of sources for free. 2021-06-05 14:53:22 +03:00			`LCase:11:11--13:41`
Remove linearity subtyping It's disappointing to have to do this, but I think necessary because various issue reports have shown it to be unsound (at least as far as inference goes) and, at the very least, confusing. This patch brings us back to the basic rules of QTT. On the one hand, this makes the 1 multiplicity less useful, because it means we can't flag arguments as being used exactly once which would be useful for optimisation purposes as well as precision in the type. On the other hand, it removes some complexity (and a hack) from unification, and has the advantage of being correct! Also, I still consider the 1 multiplicity an experiment. We can still do interesting things like protocol state tracking, which is my primary motivation at least. Ideally, if the 1 multiplicity is going to be more generall useful, we'll need some kind of way of doing multiplicity polymorphism in the future. I don't think subtyping is the way (I've pretty much always come to regret adding some form of subtyping). Fixes #73 (and maybe some others). 2020-12-27 22:58:35 +03:00			`11 \| = let 1 test = the MyNat $ case z of`
			`12 \| MyZ => MyZ`
			`13 \| (MyS k) => MyS z`
Implementations and errors - Added initial implementations for terms and values - Error messages converted to pretty printer - Colorization for error messages - Color and console width option both as command line and repl command 2020-07-28 15:11:42 +03:00
Error suggestions 2020-08-06 03:03:33 +03:00			`Suggestion: linearly bounded variables must be used exactly once.`