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

Cleanup.

parent 235bffd3
module issues.CannotFindImplementation
public export
interface Monad m => ContainerMonad m where
interface Functor m => FooBar m where
Elem : {A : Type} -> A -> m A -> Type
Foo : {A : Type} -> A -> m A -> Type
tagElem : {A : Type} -> (ma : m A) -> m (DPair A (\ a => a `Elem` ma))
bar : {A : Type} -> (ma : m A) -> m (DPair A (\ a => Foo a ma))
tagElemSpec : {A : Type} -> (ma : m A) -> map fst (tagElem ma) = ma
-- foobar : {A : Type} -> (ma : m A) -> map fst (bar ma) = 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