Skip to content

Instantly share code, notes, and snippets.

@yoshihiro503

yoshihiro503/Repeats.v

Created January 26, 2013 06:41
Show Gist options
  • Save yoshihiro503/4640609 to your computer and use it in GitHub Desktop.
Save yoshihiro503/4640609 to your computer and use it in GitHub Desktop.
Download ZIP
#proofcafe
Raw
Repeats.v
Inductive repeats {X:Type} : list X -> Prop :=
| RP_hd : forall x xs, appears_in x xs -> repeats (x::xs)
| RP_tl : forall x xs, repeats xs -> repeats (x :: xs)
.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment