git.iko.soy/Idris-dev
on 02de034 help sign in
Idris-dev/test/tutorial001/tutorial001.idr
9 lines 178 B history raw
1foo : Int -> Int
2foo x = case isLT of
3 Yes => x*2
4 No => x*4
5 where
6 data MyLT = Yes | No
7 isLT : MyLT
8 isLT = if x < 20 then Yes else No