Skip to content

Instantly share code, notes, and snippets.

@infinisil

infinisil/choice.idr

Created April 26, 2017 15:02
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/0ca06c10bfe64a627b53c124a8aeb1fe to your computer and use it in GitHub Desktop.
Save infinisil/0ca06c10bfe64a627b53c124a8aeb1fe to your computer and use it in GitHub Desktop.
Download ZIP
Raw
choice.idr
import Data.Vect
data Choice : (n : Nat) -> (k : Nat) -> Type
Arrows' : Vect n Type -> Type -> Type
Arrows' [] x = x
Arrows' (y :: xs) x = y -> Arrows' xs x
inc : (n : Nat) -> Vect n Nat
inc Z = []
inc n@(S k) = n :: inc k
Choose : Nat -> Nat -> Type
Choose n k = Arrows' (map Fin (inc n)) (Choice n k)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment