Skip to content
Snippets Groups Projects

Print, Check und left/right allgemeiner

1 file
+ 11
3
Compare changes
  • Side-by-side
  • Inline
+ 11
3
@@ -178,11 +178,11 @@
@@ -178,11 +178,11 @@
</tr>
</tr>
<tr>
<tr>
<td>left</td>
<td>left</td>
<td>If the goal is the disjunction <code>A \/ B</code>, replace it with a new subgoal <code>A</code>. This is equivalent to <code>apply or_introl</code>.</td>
<td>Uses the first constructor to prove the target. E.g. if the goal is the disjunction <code>A \/ B</code>, replace it with a new subgoal <code>A</code>. This is equivalent to <code>apply or_introl</code>.</td>
</tr>
</tr>
<tr>
<tr>
<td>right</td>
<td>right</td>
<td>If the goal is the disjunction <code>A \/ B</code>, replace it with a new subgoal <code>B</code>. This is equivalent to <code>apply or_intror</code>.</td>
<td>Uses the second constructor to prove the target. E.g. if the goal is the disjunction <code>A \/ B</code>, replace it with a new subgoal <code>B</code>. This is equivalent to <code>apply or_intror</code>.</td>
</tr>
</tr>
<tr>
<tr>
<td>contradiction</td>
<td>contradiction</td>
@@ -194,7 +194,7 @@
@@ -194,7 +194,7 @@
</tr>
</tr>
<tr>
<tr>
<td>constructor</td>
<td>constructor</td>
<td>Apply a matching constructor.</td>
<td>Apply the first matching constructor.</td>
</tr>
</tr>
</table>
</table>
@@ -220,6 +220,14 @@
@@ -220,6 +220,14 @@
<td>Unset Printing Notations</td>
<td>Unset Printing Notations</td>
<td>Do not print notations (like <code>+</code>) but show the actual function names (like <code>addn</code>) instead.</td>
<td>Do not print notations (like <code>+</code>) but show the actual function names (like <code>addn</code>) instead.</td>
</tr>
</tr>
 
<tr>
 
<td>Print ev</td>
 
<td>Shows the definition of <code>ev</code></td>
 
</tr>
 
<tr>
 
<td>Check true</td>
 
<td>Shows the type of <code>true</code></td>
 
</tr>
</table>
</table>
</body>
</body>
</html>
</html>
Loading