mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-25 04:33:45 +03:00
14 lines
283 B
Idris
14 lines
283 B
Idris
|
interface Natty (n : Nat) where
|
||
|
|
|
||
|
|
fromNatty : Type -> Nat
|
||
|
|
fromNatty (Natty Z) = Z
|
||
|
|
fromNatty (Natty (S n)) = S (fromNatty (Natty n))
|
||
|
|
fromNatty _ = Z
|
||
|
|
|
||
|
|
main : IO ()
|
||
|
|
main = ignore $ traverse printLn
|
||
|
|
[ fromNatty (Natty 3)
|
||
|
|
, fromNatty (Natty (2 + 6))
|
||
|
|
, fromNatty (List (Natty 1))
|
||
|
|
]
|