mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-17 16:21:46 +03:00
23 lines
223 B
Idris
23 lines
223 B
Idris
module Doc
|
|
|
|
||| World!
|
|
export
|
|
world : Nat -> Nat
|
|
world x = x*2
|
|
|
|
nope : Nat
|
|
nope = 0
|
|
|
|
export
|
|
||| Hello!
|
|
hello : Int -> Int
|
|
hello x = x*2
|
|
|
|
namespace NS
|
|
|
|
namespace NestedNS
|
|
|
|
||| A type of Foo
|
|
Foo : Type
|
|
Foo = ()
|