Skip to content

Instantly share code, notes, and snippets.

@edsko

edsko/TerminationMeasure.hs

Created November 7, 2017 10:21
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 edsko/77196701966333b4852a2cbbe1c7d862 to your computer and use it in GitHub Desktop.
Save edsko/77196701966333b4852a2cbbe1c7d862 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
TerminationMeasure.hs
{-@ data List [listLen] a = Nil | Cons { hd :: a , tl :: List a } @-}
data List a = Nil | Cons a (List a)
{-@ measure listLen @-}
{-@ listLen :: List a -> Nat @-}
listLen :: List a -> Int
listLen Nil = 0
listLen (Cons _ cs) = 1 + listLen cs
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment