Skip to content

Instantly share code, notes, and snippets.

@jfdm
Created March 17, 2022 10:39
Show Gist options
  • Save jfdm/48ce56125005f553c0cb5fdb5930205a to your computer and use it in GitHub Desktop.
Save jfdm/48ce56125005f553c0cb5fdb5930205a to your computer and use it in GitHub Desktop.
Different ways on doing Decidable Equality on a 'Simple' record type.
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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment