git.iko.soy/Idris-dev
on 385dcbf help sign in
Idris-dev/test/syntax002/syntax002.idr
22 lines 420 B history raw
2decl syntax fun {n} ":" [ty] "=" [def]
3 = n : ty
4 n = def
6decl syntax newtype {tname} "=" {conname} [tysyn]
7 = data tname = conname tysyn
9decl syntax EmptyShow {n} =
10 implementation Show n where
11 show x = "Nothing"
13fun add : (Int -> Int -> Int) = \x, y => x + y
15newtype Foo = MkFoo Int
17EmptyShow Foo
19main : IO ()
20main = do printLn (MkFoo 42)
21 printLn (add 3 4)