From d60ad6a22748d623667064cecc6332b4093c3db7 Mon Sep 17 00:00:00 2001 From: kl-i Date: Thu, 29 Jul 2021 23:02:28 +0100 Subject: [PATCH] Fixed hint block in Trinitarianism/Quest2.md --- Trinitarianism/Quest2.md | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/Trinitarianism/Quest2.md b/Trinitarianism/Quest2.md index 2ac137c..ad3c69e 100644 --- a/Trinitarianism/Quest2.md +++ b/Trinitarianism/Quest2.md @@ -14,10 +14,13 @@ which means from now on you can write `0 + 1` and so on (with spaces). Try coming up with a sensible definition. It may not look 'the same' as ours. +

- Hint - `n + 0` should be `n` and `n + (m + 1)` should be `(n + m) + 1` +Hint + +`n + 0` should be `n` and `n + (m + 1)` should be `(n + m) + 1`
+

Now we can make the statement: ```agda