git.iko.soy/Idris-dev
on master help sign in
'Reject' cases to default arg substitution tests.
e672357Timo Petteri Sinnemäki
test/proof005/DefaultArgSubstitutionSuccess.idr+17
compare with master
unifiedsplit
@@ -16,12 +16,29 @@ argsAreSame : (n:Nat) -> (m:Nat)
16 -> { default (decProof (decEq m n)) same : (m=n) } -> ()
16 -> { default (decProof (decEq m n)) same : (m=n) } -> ()
17argsAreSame _ _ = ()
17argsAreSame _ _ = ()
18
18
19+
20+argsAreDiff : (n:Nat) -> (m:Nat)
21+ -> { default (decProof (decEq m n)) same : (m=n) -> _|_ } -> ()
22+argsAreDiff _ _ = ()
23+
24+
19data SameNats : Type where
25data SameNats : Type where
20 same : (n:Nat) -> (m:Nat) ->
26 same : (n:Nat) -> (m:Nat) ->
21 { default (decProof (decEq m n)) same : (m=n) } -> SameNats
27 { default (decProof (decEq m n)) same : (m=n) } -> SameNats
22
28
29+data DiffNats : Type where
30+ diff : (n:Nat) -> (m:Nat) ->
31+ { default (decProof (decEq m n)) same : (m=n) -> _|_ } -> DiffNats
32+
33+
23zArgsAreSame : ()
34zArgsAreSame : ()
24zArgsAreSame = argsAreSame Z Z
35zArgsAreSame = argsAreSame Z Z
25
36
37+zszArgsAreDiff : ()
38+zszArgsAreDiff = argsAreDiff Z (S Z)
39+
26sameNatZs : SameNats
40sameNatZs : SameNats
27sameNatZs = same Z Z
41sameNatZs = same Z Z
42+
43+diffNatsZSZ : DiffNats
44+diffNatsZSZ = diff Z (S Z)
test/proof006/DefaultArgSubstitutionSyntax.idr+19
@@ -15,16 +15,35 @@ DecType {a} _ = a
15syntax "{{" [prfname] ":" "accept" [dec] "}}" "->" [ret]
15syntax "{{" [prfname] ":" "accept" [dec] "}}" "->" [ret]
16 = { default (decProof dec) prfname : DecType dec } -> ret
16 = { default (decProof dec) prfname : DecType dec } -> ret
17
17
18+syntax "{{" [prfname] ":" "reject" [dec] "}}" "->" [ret]
19+ = { default (decProof dec) prfname : DecType dec -> _|_ } -> ret
20+
18
21
19argsAreSame : (n:Nat) -> (m:Nat)
22argsAreSame : (n:Nat) -> (m:Nat)
20 -> {{ same : accept (decEq n m) }} -> ()
23 -> {{ same : accept (decEq n m) }} -> ()
21argsAreSame _ _ = ()
24argsAreSame _ _ = ()
22
25
26+
27+argsAreDiff : (n:Nat) -> (m:Nat)
28+ -> {{ diff : reject (decEq m n) }} -> ()
29+argsAreDiff _ _ = ()
30+
31+
23data SameNats : Type where
32data SameNats : Type where
24 same : (n:Nat) -> (m:Nat) -> {{ same : accept (decEq m n) }} -> SameNats
33 same : (n:Nat) -> (m:Nat) -> {{ same : accept (decEq m n) }} -> SameNats
25
34
35+data DiffNats : Type where
36+ diff : (n:Nat) -> (m:Nat) -> {{ diff : reject (decEq m n) }} -> DiffNats
37+
38+
26zArgsAreSame : ()
39zArgsAreSame : ()
27zArgsAreSame = argsAreSame Z Z
40zArgsAreSame = argsAreSame Z Z
28
41
42+zszArgsAreDiff : ()
43+zszArgsAreDiff = argsAreDiff Z (S Z)
44+
29sameNatZs : SameNats
45sameNatZs : SameNats
30sameNatZs = same Z Z
46sameNatZs = same Z Z
47+
48+diffNatsZSZ : DiffNats
49+diffNatsZSZ = diff Z (S Z)