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

Initial.

parent bea35f62
module Set.Set
import Control.Monad.Identity
import Decidable.Equality
import Sigma.Sigma
|||
public export
interface Set (sA : Type) where
A : Type
Elem : A -> sA -> Type
a1 : (a : A) -> Sigma sA (Elem a)
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)
|||
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
A = t
Elem x (Id y) = x = y
a1 x = MkSigma (Id x) Refl
{-
||| Id A is a finite set
implementation DecEq t => FiniteSet (Identity t) where
decElem x (Id y) = DecEq x y
---}
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