Data.Subset

Definitions

data Has : a -> List a -> Type

  Proof that a value is present in a list. This is
  isomorphic to `Data.List.Elem` but with (in my opinion)
  more fitting names for our use case.

Totality: total
Visibility: public export
Constructors:

Z : Has v (v :: vs)

S : Has v vs -> Has v (w :: vs)

Hints:

Has f fs => Cast (f t) (Eff fs t)

Has IO fs => HasIO (Free (Union fs))

Uninhabited (Has v [])

0 lemma_has_single : Has f [x] -> x = f

Totality: total
Visibility: export

drop : (ts : List a) -> Has v ts -> List a

Totality: total
Visibility: public export

negate : Neg ty => ty -> ty

  The underlying of unary minus. `-5` desugars to `negate (fromInteger 5)`.

Totality: total
Visibility: public export
Fixity Declaration: prefix operator, level 10

(-) : (ts : List a) -> (v : a) -> Has v ts => List a

  Removes an element from a list. This is used to
  calculate the list of effects after a single effect
  was properly handled.

Totality: total
Visibility: public export
Fixity Declarations:
infixl operator, level 8
prefix operator, level 10

data Subset : List a -> List a -> Type

  Proof that one set is subset of another set.
  Sets are represented by `List`. There is no gaurantee for no duplicate in list though.

Totality: total
Visibility: public export
Constructors:

Nil : Subset [] ys

(::) : Has x ys -> Subset xs ys -> Subset (x :: xs) ys

Hint: 

Subset fs fs' => Cast (Eff fs a) (Eff fs' a)

lemma_subset : Subset fs fs' -> Has f fs -> Has f fs'

Totality: total
Visibility: public export