Skip to content

Instantly share code, notes, and snippets.

@donovancrichton

donovancrichton/zerolinearholes.idr

Created July 24, 2020 20:24
Show Gist options
  • Save donovancrichton/d0aa7aabeb83f918abc8037120c2222a to your computer and use it in GitHub Desktop.
Save donovancrichton/d0aa7aabeb83f918abc8037120c2222a to your computer and use it in GitHub Desktop.
Download ZIP
@-Patterns forcing bound implicit types to 0 linearity
Raw
zerolinearholes.idr
data MyList : Type -> Type where
Nil : {a : Type} -> MyList a
(::) : {a : Type} -> a -> MyList a -> MyList a
f : MyList a -> ()
f [] = ()
f (x :: xs) = ?normal
g : MyList a -> ()
g [] = ()
g l@(x :: xs) = ?no_linearity
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment