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 ab255aa commit 6e66d30Copy full SHA for 6e66d30
theories/core/PrimStringAxioms.v.in
@@ -18,7 +18,7 @@
18
#[skip="8.20"] move: E; rewrite compare_spec.
19
#[skip="8.20"] elim: (to_list s1) (to_list s2) => [[]//|x xs IH [|y ys] //=].
20
#[skip="8.20"] rewrite Uint63Axioms.compare_def_spec /compare_def.
21
-#[skip="8.20"] move: (eqb_correct x y); case: eqb => [/(_ isT)->|_].
+#[skip="8.20"] move: (eqb_correct x y); case: PrimInt63.eqb => [/(_ isT)->|_].
22
#[skip="8.20"] suff: ltb y y = false by move=> -> /IH ->.
23
#[skip="8.20"] have [+ _] := ltb_spec y y.
24
#[skip="8.20"] by case: ltb => // /(_ isT); case: (to_Z y) => //=; elim.
0 commit comments