
  0 | module Data.Refined
  1 | 
  2 | import public Control.Relation
  3 | import public Control.Relation.ReflexiveClosure
  4 | import public Data.List
  5 | import public Data.Refined.List
  6 | import public Data.Refined.Nat
  7 | import public Data.Refined.Core
  8 | import public Decidable.HDecEq
  9 | 
 10 | %default total
 11 | 
 12 | public export %inline
 13 | {v : a} -> HDecEq a => HDec0 a (v ===) where
 14 |   hdec0 = hdecEq v
 15 | 
 16 | %inline refl : (0 p : a === b) -> a === b
 17 | refl Refl = Refl
 18 | 
 19 | public export %inline
 20 | {v : a} -> HDecEq a => HDec a (v ===) where
 21 |   hdec x = case hdecEq v x of
 22 |     Just0 rfl => Just $ refl rfl
 23 |     Nothing0  => Nothing
 24 |