Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
coNatIntro : (a -> Either () a) -> a -> CoNat
coNatIntro f a = case f a of
Left () -> cO
Right a' -> cS (coNatIntro f a')
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment