Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Magic pattern-matching on `Elem`
import Data.String
import Data.List
import Data.List.Elem
import Decidable.Decidable
import Decidable.Equality
%default total
toWitness : (prf1 : Dec a) -> IsYes prf1 -> a
toWitness (Yes prf2) x = prf2
fromString : (k : String) ->
{ks : List String} ->
IsYes (k `isElem` ks) =>
k `Elem` ks
fromString k @{p} = toWitness _ p
Example : List String
Example = ["0", "1", "2"]
mycase : {0 s : String} -> s `Elem` Example -> Nat
mycase "0" = 0
mycase "1" = 1
mycase "2" = 2
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment