git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/test/proof006/DefaultArgSubstitutionSyntax.idr
49 lines 1.2 kB history raw
1module DefaultArgSubstitutionSyntax
3DecProofType : {a:Type} -> Dec a -> Type
4DecProofType {a} (Yes _) = a
5DecProofType {a} (No _) = a -> Void
7decProof : {a:Type} -> (dec : Dec a) -> DecProofType dec
8decProof (Yes x) = x
9decProof (No x) = x
11DecType : {a:Type} -> Dec a -> Type
12DecType {a} _ = a
15syntax "{{" [prfname] ":" "accept" [dec] "}}" "->" [ret]
16 = { default (decProof dec) prfname : DecType dec } -> ret
18syntax "{{" [prfname] ":" "reject" [dec] "}}" "->" [ret]
19 = { default (decProof dec) prfname : DecType dec -> Void } -> ret
22argsAreSame : (n:Nat) -> (m:Nat)
23 -> {{ same : accept (decEq n m) }} -> ()
24argsAreSame _ _ = ()
27argsAreDiff : (n:Nat) -> (m:Nat)
28 -> {{ diff : reject (decEq m n) }} -> ()
29argsAreDiff _ _ = ()
32data SameNats : Type where
33 same : (n:Nat) -> (m:Nat) -> {{ same : accept (decEq m n) }} -> SameNats
35data DiffNats : Type where
36 diff : (n:Nat) -> (m:Nat) -> {{ diff : reject (decEq m n) }} -> DiffNats
39zArgsAreSame : ()
40zArgsAreSame = argsAreSame Z Z
42zszArgsAreDiff : ()
43zszArgsAreDiff = argsAreDiff Z (S Z)
45sameNatZs : SameNats
46sameNatZs = same Z Z
48diffNatsZSZ : DiffNats
49diffNatsZSZ = diff Z (S Z)