From 6a0d7f5c434c3564d0119befb6799fd77581050a Mon Sep 17 00:00:00 2001 From: Paul Oliver Date: Fri, 3 Jan 2025 11:01:20 -0800 Subject: Initial --- ch15_15.4-i.hs | 10 ++++++++++ 1 file changed, 10 insertions(+) create mode 100644 ch15_15.4-i.hs (limited to 'ch15_15.4-i.hs') diff --git a/ch15_15.4-i.hs b/ch15_15.4-i.hs new file mode 100644 index 0000000..273753d --- /dev/null +++ b/ch15_15.4-i.hs @@ -0,0 +1,10 @@ +-- Exercise 15.4-i +-- Give instances of `SDecide` for `Maybe`. + +-- This is slightly different to Sandy's version but I feel it should work the +-- same. I can't easily test if it compiles though. Importing +-- `Data.Singletons.Decide` pulls in the already existing instances! +instance SDecide a => SDecide (Maybe a) where + SJust a %~ SJust b = a %~ b + SNothing %~ SNothing = Proved Refl + _ %~ _ = Disproved $ const undefined -- cgit v1.2.1