[ fix ] some mistakes

[spcfox]

This should be an example of an implicit argument

idris2-tutorial/src/Tutorial/Eq.md

Lines 486 to 499 in 1c89da7

	### A Note of Caution: Lowercase Identifiers in Function Types
	When writing down the types of proofs as we did above, one
	has to be very careful not to fall into the following trap:
	In general, Idris will treat lowercase identifiers in
	function types as type parameters (erased implicit arguments).
	For instance, here is a try at proofing the identity functor
	law for `Maybe`:
	```idris
	mapMaybeId1 : (ma : Maybe a) -> map Prelude.id ma = ma
	mapMaybeId1 Nothing = Refl
	mapMaybeId1 (Just x) = ?mapMaybeId1_rhs
	```

[spcfox]

Did you mean «try it»?

idris2-tutorial/src/Tutorial/Eq.md

Line 897 in 1c89da7

(try id!), because Idris can't figure out on its own

[spcfox]

Following the old explanation:
2 * 127 = 254 % 256 - 128 = 126

The correct way to subtract 2^bitsize:
2 * 127 = 254 % 256 - 256 = -2

[stefan-hoeck]

Or it could be an implementation of the FromString:

implementation FromString Escaped where
  fromString s = MkEscaped (escape s) s Refl

I'll add this to my PR if you agree

Let's discuss this in its own PR. The two versions - your and mine - have distinct performance characteristics. In the current version of fromString, there will be no call to escape with strings where this is not required. On the other hand, fromString will not work with all string literals.

[stefan-hoeck]

Thanks a lot for these corrections.