From ee6a9e74e875064111afe10087aad08ccda2c4c3 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Fri, 30 Apr 2021 18:36:30 +0100 Subject: [PATCH] doc: fix typos (#379) --- doc/array.md | 2 +- doc/typeclass.md | 6 ++---- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/doc/array.md b/doc/array.md index 18a77cdb01..31182469ca 100644 --- a/doc/array.md +++ b/doc/array.md @@ -12,7 +12,7 @@ but its execution time representation is optimized, and it is similar to C++ `st The Lean type checker has no special support for reducing `Array`s. You can create arrays in several ways. You can create a small array by listing consecutive values between -`#[` and `]` and separated by colons, as shown in the following examples. +`#[` and `]` and separated by commas, as shown in the following examples. ```lean #check #[1, 2, 3] -- Array Nat diff --git a/doc/typeclass.md b/doc/typeclass.md index 2fb85a6308..38315f6015 100644 --- a/doc/typeclass.md +++ b/doc/typeclass.md @@ -221,11 +221,9 @@ instance [Inhabited b] : Inhabited (a -> b) where ``` As an exercise, try defining default instances for other types, such as `List` and `Sum` types. -The Lean standard library contains the definition `inferInstance`. It has type `{α : Type u} → [i : α] → α`, +The Lean standard library contains the definition `inferInstance`. It has type `{α : Sort u} → [i : α] → α`, and is useful for triggering the type class resolution procedure when the expected type is an instance. ```lean -#check @inferInstance -- {α : Type u} → [i : α] → α - #check (inferInstance : Inhabited Nat) -- Inhabited Nat def foo : Inhabited (Nat × Nat) := @@ -354,7 +352,7 @@ instance [HMul α β γ] : HMul α (Array β) (Array γ) where #eval hMul 4 3 -- 12 #eval hMul 4 #[2, 3, 4] -- #[8, 12, 16] -#eval hMul (-2) #[3, -1, 4] -- #[-6, 2, -4] +#eval hMul (-2) #[3, -1, 4] -- #[-6, 2, -8] #eval hMul 2 #[#[2, 3], #[0, 4]] -- #[#[4, 6], #[0, 8]] # end Ex ```