Skip to content

Instantly share code, notes, and snippets.

@edwinb

edwinb/inBound.idr

Created November 25, 2012 21:15
Show Gist options
  • Save edwinb/4145388 to your computer and use it in GitHub Desktop.
Save edwinb/4145388 to your computer and use it in GitHub Desktop.
Download ZIP
List bounds
Raw
inBound.idr
using (xs : List a)
data InBound : Nat -> List a -> Set where
inO : InBound O (x :: xs)
inS : InBound k xs -> InBound (S k) (x :: xs)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment