Fixed hint block in Trinitarianism/Quest2.md
This commit is contained in:
parent
064691b029
commit
d60ad6a227
@ -14,10 +14,13 @@ which means from now on you can write `0 + 1`
|
|||||||
and so on (with spaces).
|
and so on (with spaces).
|
||||||
Try coming up with a sensible definition.
|
Try coming up with a sensible definition.
|
||||||
It may not look 'the same' as ours.
|
It may not look 'the same' as ours.
|
||||||
|
<p>
|
||||||
<details>
|
<details>
|
||||||
<summary>Hint</summary>
|
<summary>Hint</summary>
|
||||||
`n + 0` should be `n` and `n + (m + 1)` should be `(n + m) + 1`
|
|
||||||
|
`n + 0` should be `n` and `n + (m + 1)` should be `(n + m) + 1`
|
||||||
</details>
|
</details>
|
||||||
|
</p>
|
||||||
|
|
||||||
Now we can make the statement:
|
Now we can make the statement:
|
||||||
```agda
|
```agda
|
||||||
|
Loading…
Reference in New Issue
Block a user