Commit cb86ed59 authored by Nicola Botta's avatar Nicola Botta
Browse files

Cleanup.

parent 7221c669
......@@ -2,37 +2,67 @@ module Set.Set
import Control.Monad.Identity
import Decidable.Equality
import Data.List
import Sigma.Sigma
|||
public export
interface Set (sA : Type) where
interface Set t st where
Elem : t -> st -> Type
a1 : (x : t) -> Sigma st (Elem x)
Empty : st -> Type
Empty xs = (x : t) -> Not (Elem x xs)
Equal : st -> st -> Type
Equal xs ys = ((x : t) -> Elem x xs -> Elem x ys, (y : t) -> Elem y ys -> Elem y xs)
A : Type
Elem : A -> sA -> Type
interface Set t st => FiniteSet t st where
a1 : (a : A) -> Sigma sA (Elem a)
decEqual : (xs, ys : st) -> Dec (Equal xs xs)
Empty : sA -> Type
Empty as = (a : A) -> Not (Elem a as)
Equal : sA -> sA -> Type
Equal xs ys = ((a : A) -> Elem a xs -> Elem a ys, (a : A) -> Elem a ys -> Elem a xs)
implementation FiniteSet t st => Eq st where
xs == ys with (decEqual xs ys)
xs == ys | (Yes p) = True
xs == ys | (No c) = False
implementation Set t (Identity t) where
Elem x (Id y) = x = y
a1 x = ?kika -- MkSigma (Id x) Refl
{-
implementation Set t (List t) where
Elem = Data.List.Elem
a1 x = ?guga -- MkSigma [x] Here
---}
{-
|||
public export
interface Set sA => FiniteSet sA where
decElem : (a : A) -> (as : sA) -> Dec (Elem a as)
---}
-- Examples:
{-
||| Identity A set
implementation Set (Identity t) where
......@@ -43,8 +73,6 @@ implementation Set (Identity t) where
a1 x = MkSigma (Id x) Refl
{-
||| Id A is a finite set
implementation DecEq t => FiniteSet (Identity t) where
......
......@@ -5,7 +5,7 @@ interface Foo (sA : Type) where
A : Type
Elem : A -> sA -> Type
Empty : sA -> Type
-- Empty as = (a : A) -> Not (Elem a as)
--Empty as = (a : A) -> Not (Elem a as)
public export
implementation Foo (Identity Bool) where
......
import Data.List
-- import Data.List.Elem
interface Set t st where
Elem : t -> st -> Type
a1 : (x : t) -> DPair st (Elem x)
a2 : (x : t) -> (xs : st) -> Dec (Elem x xs)
Empty : st -> Type
Empty xs = (x : t) -> Not (Elem x xs)
import Control.Monad.Identity
interface Set t st where
Elem : t -> st -> Type
a1 : (x : t) -> DPair st (Elem x)
Empty : st -> Type
Empty xs = (x : t) -> Not (Elem x xs)
Equal : st -> st -> Type
Equal xs ys = ((x : t) -> Elem x xs -> Elem x ys, (y : t) -> Elem y ys -> Elem y xs)
implementation Set t (Identity t) where
Elem x (Id y) = x = y
a1 x = MkDPair (Id x) Refl
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