Commit 83219b4b authored by Nicola Botta's avatar Nicola Botta
Browse files

Cleanup.

parent a3144124
......@@ -3,10 +3,10 @@ module issues.FiniteAsFatInterface
import Data.Fin
import Data.Vect
tail : {A : Type} -> {n : Nat} -> (Fin (S n) -> A) -> (Fin n -> A)
tail : {0 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 : {0 A : Type} -> {n : Nat} -> (Fin n -> A) -> Vect n A
toVect {n = Z} _ = Nil
toVect {n = S m} f = (f FZ) :: (toVect (tail f))
......
......@@ -3,10 +3,10 @@ module issues.FiniteAsInterface
import Data.Fin
import Data.Vect
tail : {A : Type} -> {n : Nat} -> (Fin (S n) -> A) -> (Fin n -> A)
tail : {0 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 : {0 A : Type} -> {n : Nat} -> (Fin n -> A) -> Vect n A
toVect {n = Z} _ = Nil
toVect {n = S m} f = (f FZ) :: (toVect (tail f))
......@@ -17,9 +17,11 @@ record Iso a b where
toFrom : (y : b) -> to (from y) = y
fromTo : (x : a) -> from (to x) = x
---
interface Finite t where
card : Nat
iso : Iso t (Fin card)
foo : (Finite t) => Vect (card t) t
foo : (Finite t) => Vect (card {t}) t
foo = toVect (from iso)
......@@ -3,10 +3,10 @@ module issues.FiniteAsRecord
import Data.Fin
import Data.Vect
tail : {A : Type} -> {n : Nat} -> (Fin (S n) -> A) -> (Fin n -> A)
tail : {0 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 : {0 A : Type} -> {n : Nat} -> (Fin n -> A) -> Vect n A
toVect {n = Z} _ = Nil
toVect {n = S m} f = (f FZ) :: (toVect (tail f))
......@@ -22,5 +22,5 @@ record Finite t where
card : Nat
iso : Iso t (Fin card)
foo : (Finite t) => Vect (card t) t
foo = toVect (from iso)
foo : (ft : Finite t) -> Vect (card ft) t
foo ft = toVect (from (iso ft))
......@@ -3,10 +3,10 @@ module issues.FiniteAsSigmaType
import Data.Fin
import Data.Vect
tail : {A : Type} -> {n : Nat} -> (Fin (S n) -> A) -> (Fin n -> A)
tail : {0 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 : {0 A : Type} -> {n : Nat} -> (Fin n -> A) -> Vect n A
toVect {n = Z} _ = Nil
toVect {n = S m} f = (f FZ) :: (toVect (tail f))
......@@ -17,6 +17,8 @@ record Iso a b where
toFrom : (y : b) -> to (from y) = y
fromTo : (x : a) -> from (to x) = x
---
Finite : Type -> Type
Finite t = DPair Nat (\ n => Iso t (Fin n))
......
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