Skip to content

Instantly share code, notes, and snippets.

@infinisil

infinisil/choice.idr

Created April 26, 2017 15:16
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 infinisil/f275566604f9f38d9544b3a331f3b21e to your computer and use it in GitHub Desktop.
Save infinisil/f275566604f9f38d9544b3a331f3b21e to your computer and use it in GitHub Desktop.
Download ZIP
Raw
choice.idr
import Data.Vect
ChooseType : (n : Nat) -> (k : Nat) -> {auto ok : LTE k n} -> Type
ChooseType n Z {ok=LTEZero} = ()
ChooseType n@(S ns) (S Z) {ok=(LTESucc oks)} = Fin n
ChooseType n@(S ns) (S ks) {ok=(LTESucc oks)} = (Fin n, ChooseType ns ks)
data Choice : (n : Nat) -> (k : Nat) -> Type where
Choose : (n : Nat) -> (k : Nat) -> { auto ok : LTE k n } ->
ChooseType n k -> Choice n k
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment