Skip to content

Commit 9fe2393

Browse files
hrutvikmn200
authored andcommitted
[cheatsheet] Fix a couple of underscores
These were being converted into `<em>` tags. Use HTML escape codes instead.
1 parent 6213adb commit 9fe2393

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

Manual/Cheatsheet/cheatsheet.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -390,7 +390,7 @@ In many cases, we may want to state exactly how the goal should be taken apart (
390390
<code>qrefinel [&grave;<i>term</i>&grave;s]</code>
391391
: Like `qrefine`, but accepts a list of terms to instantiate multiple `∃` quantifiers.
392392
Also can be passed underscores, to avoid refining selected `∃` quantifiers.
393-
For example, for a goal `n = 2 /\ c = 5 ==> ∃ a b c d. a + b = c + d`, the tactic <code>strip_tac >> qrefinel [&grave;_&grave;,&grave;SUC c&grave;,&grave;_&grave;,&grave;n + m&grave;]</code> produces the new goal `∃ a c' m. a + SUC c = c' + (n + m)` .
393+
For example, for a goal `n = 2 /\ c = 5 ==> ∃ a b c d. a + b = c + d`, the tactic <code>strip_tac >> qrefinel [&grave;&#95;&grave;,&grave;SUC c&grave;,&grave;&#95;&grave;,&grave;n + m&grave;]</code> produces the new goal `∃ a c' m. a + SUC c = c' + (n + m)` .
394394
395395
<code>goal_assum $ drule_at Any</code>
396396
: For a goal of the form `∃ vars . P1 /\ ... /\ Pn` (where the `vars` may be free in the `Pi`), attempts to match the `Pi` against the assumptions.

0 commit comments

Comments
 (0)