Commit 58ecca71 authored by Nicola Botta's avatar Nicola Botta
Browse files

Cleanup.

parent 235bffd3
......@@ -21,5 +21,5 @@ interface Finite t where
card : Nat
iso : Iso t (Fin card)
foo : (Finite t) => Vect card t
foo : (Finite t) => Vect (card t) t
foo = toVect (from iso)
module issues.FiniteAsRecord
import Data.Fin
import Data.Vect
tail : {A : Type} -> {n : Nat} -> (Fin (S n) -> A) -> (Fin n -> A)
tail f = f . FS
toVect : {A : Type} -> {n : Nat} -> (Fin n -> A) -> Vect n A
toVect {n = Z} _ = Nil
toVect {n = S m} f = (f FZ) :: (toVect (tail f))
record Iso a b where
constructor MkIso
to : a -> b
from : b -> a
toFrom : (y : b) -> to (from y) = y
fromTo : (x : a) -> from (to x) = x
record Finite t where
constructor MkFinite
card : Nat
iso : Iso t (Fin card)
foo : (Finite t) => Vect (card t) t
foo = 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