0 | ||| An example implementation for the Tolerance relation.
 1 |
 2 | module Data.Nat.Order.Relation
 3 |
 4 | import Control.Relation
 5 |
 6 | Adjacent : (a, b : Nat) -> Type
 7 | Adjacent a b = Either (a = b) $ Either (a = S b) (b = S a)
 8 |
 9 | Reflexive Nat Adjacent where
10 |   reflexive = Left Refl
11 |
12 | Symmetric Nat Adjacent where
13 |   symmetric (Left x_eq_y) = Left $ sym x_eq_y
14 |   symmetric (Right $  Left prf) = Right $ Right prf
15 |   symmetric (Right $ Right prf) = Right $  Left prf
16 |
17 | Tolerance Nat Adjacent where
18 |