fixed hint
This commit is contained in:
parent
639b903670
commit
8ef93f790b
1 changed files with 2 additions and 2 deletions
|
@ -791,8 +791,8 @@ and back is the identity:
|
||||||
to (from b) ≡ b
|
to (from b) ≡ b
|
||||||
|
|
||||||
(Hint: For each of these, you may first need to prove related
|
(Hint: For each of these, you may first need to prove related
|
||||||
properties of `One`. Also, you may need to prove that `1` is
|
properties of `One`. Also, you may need to prove that
|
||||||
less or equal to the result of `from b`.)
|
if `One b` then `1` is less or equal to the result of `from b`.)
|
||||||
|
|
||||||
```
|
```
|
||||||
-- Your code goes here
|
-- Your code goes here
|
||||||
|
|
Loading…
Reference in a new issue