Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
import Data.Vect
-- let us pretend we have written this function
postulate vectorsInits : Vect n t -> Vect n (p : Fin k ** Vect (finToNat p) t)
total
contra : Void
contra with (vectorsInits {k = 0} [42])
contra | [(x ** _)] = absurd x
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment