Created
March 17, 2022 10:39
-
-
Save jfdm/48ce56125005f553c0cb5fdb5930205a to your computer and use it in GitHub Desktop.
Different ways on doing Decidable Equality on a 'Simple' record type.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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