Different ways on doing Decidable Equality on a 'Simple' record type.

Examples.idr

module Examples

import Decidable.Equality

data Foo = F String Nat

namespace Beginner
  export
  decEq : (x,y : Foo) -> Dec (x = y)
  decEq (F xs xn) (F ys yn) with (decEq xs ys)
    decEq (F xs xn) (F xs yn) | (Yes Refl) with (decEq xn yn)
      decEq (F xs xn) (F xs xn) | (Yes Refl) | (Yes Refl)
        = Yes Refl
      decEq (F xs xn) (F xs yn) | (Yes Refl) | (No contra)
        = No (\Refl => contra Refl)
    decEq (F xs xn) (F ys yn) | (No contra)
      = No (\Refl => contra Refl)

namespace Intermediate

  -- Provided by Matus, and encapsulated in my Toolkit as `Toolkit.Decidable.Do`.

  otherwise : Dec b -> (a -> b) -> Either (Not a) b
  otherwise (Yes pfB)  f = Right pfB
  otherwise (No notB)  f = Left (notB . f)

  decDo : Either (Not a) a -> Dec a
  decDo (Left notA) = No notA
  decDo (Right pfA) = Yes pfA

  export
  decEq : (x,y : Foo) -> Dec (x = y)
  decEq (F xs xn) (F ys yn)
    = decDo $ do Refl <- decEq xs ys `otherwise` (\Refl => Refl)
                 Refl <- decEq xn yn `otherwise` (\Refl => Refl)
                 pure Refl


namespace Novice

  export
  decEq : (x,y : Foo) -> Dec (x = y)
  decEq (F xs xn) (F ys yn) with (decEq (xs,xn) (ys,yn))
    decEq (F xs xn) (F xs xn) | (Yes Refl)
      = Yes Refl
    decEq (F xs xn) (F ys yn) | (No contra)
      = No (\Refl => contra Refl)