Skip to content

Instantly share code, notes, and snippets.

@righ1113

righ1113/CoInductive.idr

Created February 3, 2019 04:30
Show Gist options
  • Save righ1113/e60e325b2db0ef3158b5d8bec76f8c98 to your computer and use it in GitHub Desktop.
Save righ1113/e60e325b2db0ef3158b5d8bec76f8c98 to your computer and use it in GitHub Desktop.
Download ZIP
余帰納？
Raw
CoInductive.idr
module CoInductive
%default total
-- 性質Q
codata Q : Stream Nat -> Type where
Qcons : (x:Nat) -> Q xs -> Q (x::xs)
isQ : (xs:Stream Nat) -> Q xs
isQ (x::xs) = Qcons x (isQ xs)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment