We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent d9d85c8 commit 0e14c7bCopy full SHA for 0e14c7b
PerformanceExperiments/Sample.v
@@ -60,7 +60,7 @@ Lemma continued_fraction_correct v n
60
: eval_continued_fraction (continued_fraction v n) == v.
61
Proof.
62
cbv [eval_continued_fraction].
63
- revert v; induction n; intro; cbn; destruct (Qeq_bool 0 v) eqn:H; cbn.
+ revert v; induction n; intro; cbn -[Qeq_bool]; destruct (Qeq_bool 0 v) eqn:H; cbn.
64
all: rewrite ?Qeq_bool_iff in H; rewrite <- ?H.
65
all: try reflexivity.
66
{ rewrite (surjective_pairing (continued_fraction _ _)); cbn.
0 commit comments