git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/test/basic005/test019.lidr
16 lines 373 B history raw
1> module Main
3> ifTrue : So True -> Nat
4> ifTrue Oh = S Z
6> ifFalse : So False -> Nat
7> ifFalse Oh impossible
9> test : (f : Nat -> Bool) -> (n : Nat) -> So (f n) -> Nat
10> test f n x with (f n)
11> | True = ifTrue x
12> | False = ifFalse x
14> main : IO ()
15> main = print (test ((S 4) ==) 5 Oh)