git.iko.soy/Idris-dev
on a427f21 help sign in
Idris-dev/test/basic009/Main.idr
16 lines 195 B history raw
1module Main
3import A as X
4import B.C as Y
6checkX : X.num = Z
7checkX = Refl
9checkY : Y.num = S Z
10checkY = Refl
12checkAX : X.num = A.num
13checkAX = Refl
15checkBY : Y.num = B.C.num
16checkBY = Refl