Commit 040b2810 authored by Nicola Botta's avatar Nicola Botta
Browse files


parent 553bf1df
......@@ -32,5 +32,5 @@ toList (MkSigma _ iso) = Fin.Operations.toList (from iso)
||| Maps a finite type |A| of cardinality |n| to a vector of |A|-values of length |n|
public export
toVect : {A : Type} -> (fA : Finite A) -> Vect (card fA) A
toVect (MkSigma _ iso) = Fin.Operations.toVect (from iso)
toVect (MkSigma _ iso) = toVect (from iso)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment