Skip to content

C
cpdt
Commit f5e58b2e authored by Adam Chlipala's avatar Adam Chlipala
Browse files
Options

Spell-check

parent c94890c7
Show whitespace changes
Inline Side-by-side
Showing with 1 addition and 1 deletion
src/Predicates.v
View file @ f5e58b2e
...@@ -670,7 +670,7 @@ Abort. ...@@ -670,7 +670,7 @@ Abort.
Lemma even_contra' : forall n', even n' -> forall n, n' = S (n + n) -> False. Lemma even_contra' : forall n', even n' -> forall n, n' = S (n + n) -> False.
induction 1; crush. induction 1; crush.
(** At this point, it is useful to consider all cases of [n] and [n0] being zero or nonzero. Only one of these cases has any trickyness to it. *) (** At this point, it is useful to consider all cases of [n] and [n0] being zero or nonzero. Only one of these cases has any trickiness to it. *)
destruct n; destruct n0; crush. destruct n; destruct n0; crush.
(** [[ (** [[
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment