mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-24 20:23:11 +03:00
45a9668370
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.
15 lines
365 B
Plaintext
15 lines
365 B
Plaintext
1/2: Building Test (Test.idr)
|
|
2/2: Building As (As.idr)
|
|
As> Prelude.id : (1 _ : 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!
|