max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: fix typos (#379)

Browse source
This commit is contained in:
Kevin Buzzard 2021-04-30 18:36:30 +01:00 • committed by GitHub
parent e1cde87c43
commit ee6a9e74e8
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 3 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
doc/array.md
View file

@ -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

6
doc/typeclass.md
View file

@ -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
```