git.iko.soy/Idris-dev
on 385dcbf help sign in
Idris-dev/test/basic005/test019.lidr
18 lines 393 B history raw
1> module Main
3> import Data.So
5> ifTrue : So True -> Nat
6> ifTrue Oh = S Z
8> ifFalse : So False -> Nat
9> ifFalse Oh impossible
11> test : (f : Nat -> Bool) -> (n : Nat) -> So (f n) -> Nat
12> test f n x with (f n)
13> | True = ifTrue x
14> | False = ifFalse x
16> main : IO ()
17> main = printLn (test ((S 4) ==) 5 Oh)