Commit 310d6b1e authored by Nicola Botta's avatar Nicola Botta
Browse files

Cleanup.

parent 6f823db8
......@@ -7,6 +7,6 @@ interface Functor m => FooBar m where
bar : {A : Type} -> (ma : m A) -> m (DPair A (\ a => Foo a ma))
-- foobar : {A : Type} -> (ma : m A) -> map fst (bar ma) = ma
foobar : {A : Type} -> (ma : m A) -> map Builtin.DPair.DPair.fst (bar ma) = ma
......@@ -3,7 +3,7 @@ module issues.CannotSolveConstraint2
import Data.Fin
import Data.Vect
toVect : {A : Type} -> {n : Nat} -> (Fin n -> A) -> Vect n A
toVect : {0 A : Type} -> {0 n : Nat} -> (Fin n -> A) -> Vect n A
record Iso a b where
constructor MkIso
......
......@@ -3,10 +3,10 @@ module issues.FiniteAsInterface
import Data.Fin
import Data.Vect
tail : {0 A : Type} -> {n : Nat} -> (Fin (S n) -> A) -> (Fin n -> A)
tail : {A : Type} -> {n : Nat} -> (Fin (S n) -> A) -> (Fin n -> A)
tail f = f . FS
toVect : {0 A : Type} -> {n : Nat} -> (Fin n -> A) -> Vect n A
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))
......@@ -25,3 +25,16 @@ interface Finite t where
foo : (Finite t) => Vect (card {t}) t
foo = toVect (from iso)
toVectComplete : (Finite t) => (x : t) -> Elem x foo
toVectComplete a = s3 where
s1 : Elem (from iso (to iso a)) (toVect (from iso))
s1 = ?s1def
s2 : from iso (to iso a) = a
s2 = fromTo iso a
s3 : Elem a (toVect (from iso))
s3 = replace {p = \ z => Elem z (toVect (from iso))} s2 s1
{-
---}
module Implementation
module issues.Implementation
import Data.Fin
interface Foo t where
foo : Nat
interface Foo (t : Type) where
card : Nat
to : t -> Fin card
implementation (n : Nat) => Foo (Fin n) where
foo {n} = n
bar : Nat
bar = S card
implementation Foo (Fin k) where
card = k
to = id
{-
---}
......@@ -6,6 +6,6 @@ interface Monad m => FooBar m where
Bar : {A : Type} -> m A -> Type
foo : {A : Type} -> (a : A) -> (ma : m A) -> Foo a ma -> Bar {A} ma
foo : {A : Type} -> (a : A) -> (ma : m A) -> Foo a ma -> Bar ma
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