ALT Alexander Gryzlov's talk: "Total Functions for Automated Reasoning: Building Terminating Theorem Provers"

ALT type IsNotEq b a = Refuted (b :~: a) data IsUniqList a where IsUniqListNil :: IsUniqList '[] IsUniqListCons :: IsNotElem a as -> IsUniqList as -> IsUniqList (a : as) data IsNotElem b as where IsNotElemNil :: IsNotElem b '[] IsNotElemCons :: IsNotEq b a -> IsNotElem b as -> IsNotElem b (a : as) data UniqList a where UniqList :: IsUniqList a -> Sing a -> UniqList a decideIsNotEq :: (SDecide k) => Sing (a :: k) -> Sing (b :: k) -> Maybe (IsNotEq a b) decideIsNotEq a b = case a %~ b of Proved _ -> Nothing Disproved d -> Just d decideIsNotElem :: (SDecide k) => Sing (a :: k) -> Sing (as :: [k]) -> Maybe (IsNotElem a as) decideIsNotElem a = \case SNil -> Just IsNotElemNil SCons b bs -> case a %~ b of Proved _ -> Nothing Disproved r -> case decideIs

ALT data SomeIsElem x xs = forall y. SomeIsElem (IsElem '(x, y) xs) pLookup' :: IsElem x (Keys d) -> Sing (d :: [(k, v)]) -> SomeIsElem x d pLookup' (IsElemHead Refl) (SCons (STuple2 _ _) _) = SomeIsElem $ IsElemHead Refl pLookup' (IsElemTail q) (SCons _ d) = case pLookup' q d of SomeIsElem p -> SomeIsElem $ IsElemTail p