Skip to content

Instantly share code, notes, and snippets.

@qnighy

qnighy/unacceptable-cofixpoint.v

Created March 28, 2014 08:44
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save qnighy/9828159 to your computer and use it in GitHub Desktop.
Save qnighy/9828159 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
unacceptable-cofixpoint.v
CoInductive cnat : Set :=
| O : cnat | S : cnat -> cnat.
CoFixpoint cplus n m :=
match n with
| O => m
| S p => S (cplus p m)
end.
(* mm1 means m - 1 *)
CoFixpoint cmultp1 n mm1 :=
match n with
| O => O
| S p => S (cplus mm1 (cmultp1 p mm1))
end.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment