git.iko.soy/Idris-dev
on master help sign in
Idris-dev/test/basic020/basic020.idr
42 lines 844 B history raw
1%default total
3data Ty = Ctor Int
5fn : Ty -> Ty
6fn m@(Ctor _) = y
7 where
8 y = m -- from @ pattern
10asPatternVisibleInWhere : fn (Ctor 42) = Ctor 42
11asPatternVisibleInWhere = Refl
13fn2 : Ty -> Ty
14fn2 m@(Ctor _) = y (Ctor 99)
15 where
16 y m = m -- should be the arg `m`, not the @ pattern
18lhsVariablesShadowAsPattern : fn2 (Ctor 42) = Ctor 99
19lhsVariablesShadowAsPattern = Refl
21fn3 : Ty -> Ty
22fn3 m@(Ctor _) = y (Ctor 99)
23 where
24 y m = z
25 where
26 z = m -- should be y's arg `m`, not @ pattern
28nestedWhereShadowsAsPattern : fn3 (Ctor 42) = Ctor 99
29nestedWhereShadowsAsPattern = Refl
31fn4 : Ty -> Ty
32fn4 m@(Ctor _) = y (Ctor 99)
33 where
34 y _ = z
35 where
36 z = m -- should be @ pattern
38nestedWhereExposesAsPattern : fn4 (Ctor 42) = Ctor 42
39nestedWhereExposesAsPattern = Refl
41main : IO ()
42main = putStrLn "OK"