Idris2/tests/idris2/import005/expected

1/2: Building Test (Test.idr)
2/2: Building As (As.idr)
As> Prelude.id : a -> a
As> Prelude.Uninhabited : Type -> Type
As> Toast.pythag : Int -> List (Int, (Int, Int))
As> Toast.Inside.fact : Nat -> Nat
As> Toast.nardle : Needle a => a -> a
As> Toast.noo : Needle a => a -> a
As> 16
As> [(3, (4, 5)), (6, (8, 10))]
As> pythag
As> 24
As> 24
As> Bye for now!
Add "import X as Y" properly Instead of just the cursory name update that we used to do (which didn't work properly anyway for a lot of reasons), now we add aliases for all the names in the imported module. So, like Idris 1, every global has a canonical name by which we can refer to it, but it can also have aliases via "import ... as". 2020-07-04 22:26:49 +03:00			`1/2: Building Test (Test.idr)`
			`2/2: Building As (As.idr)`
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			`As> Prelude.id : a -> a`
Export all of the Prelude as Prelude There is an argument that, for import public, this should be automatic (that is, the publicly imported things should be reexported with the parent namespace). I decided not to do this, because another use of import public which we do a lot in the Idris 2 code base is purely as a convenience, where we still expect things to be in their original namespace. Also, where there's a choice between things being explicit and implicit, I prefer to err on the side of explicit now. So, if what you really want in an API is to reexport, you can do that, but explicitly. 2020-07-04 23:57:54 +03:00			`As> Prelude.Uninhabited : Type -> Type`
Add "import X as Y" properly Instead of just the cursory name update that we used to do (which didn't work properly anyway for a lot of reasons), now we add aliases for all the names in the imported module. So, like Idris 1, every global has a canonical name by which we can refer to it, but it can also have aliases via "import ... as". 2020-07-04 22:26:49 +03:00			`As> Toast.pythag : Int -> List (Int, (Int, Int))`
			`As> Toast.Inside.fact : Nat -> Nat`
			`As> Toast.nardle : Needle a => a -> a`
			`As> Toast.noo : Needle a => a -> a`
			`As> 16`
			`As> [(3, (4, 5)), (6, (8, 10))]`
			`As> pythag`
			`As> 24`
			`As> 24`
			`As> Bye for now!`