Skip to content

Instantly share code, notes, and snippets.

@infinisil

infinisil/choice.idr

Created April 26, 2017 14:26
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/503a8d670c1fe407c2c19d339ed4eca1 to your computer and use it in GitHub Desktop.
Save infinisil/503a8d670c1fe407c2c19d339ed4eca1 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
choice.idr
ChooseType : (n : Nat) -> (k : Nat) -> {auto ok : LTE k n} -> Type
ChooseType n Z {ok=LTEZero} = ()
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