Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
syntax mmatch [t] as {x} returning [ty] cases [cs] =
Match (\x => ty) t cs
syntax pat {x} "." [tm] = PTele (\x => tm)
syntax [tm1] "=>" [tm2] = PBase tm1 tm2
foo : Tac (List ())
foo = mmatch Z as y returning (List ())
cases [
pat x . pat y . pat z . ((x + y) +z) => return [(), ()]
, pat x . x => return []
]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.