Commit 2bc64553 authored by simonpj's avatar simonpj
Browse files

Comments

parent d88b0b67
......@@ -18,3 +18,7 @@ foo = ntI (`eqE` (eqI :: EQ_ m n))
-- This works:
-- foo = ntI (\eq -> eq `eqE` (eqI :: EQ_ m n))
-- eq :: EQ_ (Maybe m) (Maybe n)
-- Need (Maybe m ~ Maybe n) => EQ_ m n ~ EQ_ zeta zeta
-- which redues to (m~n) => m ~ zeta
-- but then we are stuck
\ No newline at end of file
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