git.iko.soy/Idris-dev
on master help sign in
'Reject' cases to default arg substitution tests.
commite672357fcc2c5e106118c5424455b36b2c49f54d authorTimo Petteri Sinnemäki <timo.sinnemaki@helsinki.fi> dateSun 6 Apr 2014, 02:06 (13 years ago) parent4624be2
2 files changed+36
compare with master
unifiedsplit
test/proof005/DefaultArgSubstitutionSuccess.idr+17 test/proof006/DefaultArgSubstitutionSyntax.idr+19
test/proof005/DefaultArgSubstitutionSuccess.idr+17
@@ -16,12 +16,29 @@ argsAreSame : (n:Nat) -> (m:Nat)
1616 -> { default (decProof (decEq m n)) same : (m=n) } -> ()
1717argsAreSame _ _ = ()
1818
19+
20+argsAreDiff : (n:Nat) -> (m:Nat)
21+ -> { default (decProof (decEq m n)) same : (m=n) -> _|_ } -> ()
22+argsAreDiff _ _ = ()
23+
24+
1925data SameNats : Type where
2026 same : (n:Nat) -> (m:Nat) ->
2127 { default (decProof (decEq m n)) same : (m=n) } -> SameNats
2228
29+data DiffNats : Type where
30+ diff : (n:Nat) -> (m:Nat) ->
31+ { default (decProof (decEq m n)) same : (m=n) -> _|_ } -> DiffNats
32+
33+
2334zArgsAreSame : ()
2435zArgsAreSame = argsAreSame Z Z
2536
37+zszArgsAreDiff : ()
38+zszArgsAreDiff = argsAreDiff Z (S Z)
39+
2640sameNatZs : SameNats
2741sameNatZs = 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
1515syntax "{{" [prfname] ":" "accept" [dec] "}}" "->" [ret]
1616 = { default (decProof dec) prfname : DecType dec } -> ret
1717
18+syntax "{{" [prfname] ":" "reject" [dec] "}}" "->" [ret]
19+ = { default (decProof dec) prfname : DecType dec -> _|_ } -> ret
20+
1821
1922argsAreSame : (n:Nat) -> (m:Nat)
2023 -> {{ same : accept (decEq n m) }} -> ()
2124argsAreSame _ _ = ()
2225
26+
27+argsAreDiff : (n:Nat) -> (m:Nat)
28+ -> {{ diff : reject (decEq m n) }} -> ()
29+argsAreDiff _ _ = ()
30+
31+
2332data SameNats : Type where
2433 same : (n:Nat) -> (m:Nat) -> {{ same : accept (decEq m n) }} -> SameNats
2534
35+data DiffNats : Type where
36+ diff : (n:Nat) -> (m:Nat) -> {{ diff : reject (decEq m n) }} -> DiffNats
37+
38+
2639zArgsAreSame : ()
2740zArgsAreSame = argsAreSame Z Z
2841
42+zszArgsAreDiff : ()
43+zszArgsAreDiff = argsAreDiff Z (S Z)
44+
2945sameNatZs : SameNats
3046sameNatZs = same Z Z
47+
48+diffNatsZSZ : DiffNats
49+diffNatsZSZ = diff Z (S Z)