LeifW/nthType.idr

Created March 12, 2020 12:52

Star (0) You must be signed in to star a gist
Fork (0) You must be signed in to fork a gist

Select an option

Learn more about clone URLs
Clone this repository at <script src="https://gist.github.com/LeifW/579c4eaf4e365b27b3a647890525710c.js"></script>
Save LeifW/579c4eaf4e365b27b3a647890525710c to your computer and use it in GitHub Desktop.

Download ZIP

Raw

nthType.idr

	import Data.Vect

	types : Vect 3 Type
	types = [Int,Bool,Int]

	nthType : {n: Fin 3} -> Type
	nthType = index n types

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment