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
coNatIntro : (a -> Either () a) -> a -> CoNat | |
coNatIntro f a = case f a of | |
Left () -> cO | |
Right a' -> cS (coNatIntro f a') |