Edwin Brady 45a9668370 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 21:57:54 +01:00
..
As.idr	Add "import X as Y" properly	2020-07-04 20:26:49 +01:00
expected	Export all of the Prelude as Prelude	2020-07-04 21:57:54 +01:00
input	Export all of the Prelude as Prelude	2020-07-04 21:57:54 +01:00
run	Add "import X as Y" properly	2020-07-04 20:26:49 +01:00
Test.idr	Add "import X as Y" properly	2020-07-04 20:26:49 +01:00