Skip to content

Instantly share code, notes, and snippets.

@gallais

gallais/ElemSplit.idr

Created September 30, 2021 10:16
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save gallais/6f4331fccaf475b4bfd18ff42521fbe7 to your computer and use it in GitHub Desktop.
Save gallais/6f4331fccaf475b4bfd18ff42521fbe7 to your computer and use it in GitHub Desktop.
Download ZIP
Magic pattern-matching on `Elem`
Raw
ElemSplit.idr
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