Skip to content

Instantly share code, notes, and snippets.

@david-christiansen

david-christiansen/MTac.idr

Created September 9, 2015 15:02
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 david-christiansen/34e787a19fbcd2fb0e26 to your computer and use it in GitHub Desktop.
Save david-christiansen/34e787a19fbcd2fb0e26 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
MTac.idr
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