Commit 7221c669 authored by Nicola Botta's avatar Nicola Botta
Browse files


parent d2c9703b
import Control.Monad.Identity
public export
interface Foo (sA : Type) where
A : Type
Elem : A -> sA -> Type
Empty : sA -> Type
-- Empty as = (a : A) -> Not (Elem a as)
public export
implementation Foo (Identity Bool) where
A = Bool
Elem x (Id y) = 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