In 3.5.6 , idahospiders is used in an Append example , but no mention provided on where it was defined had me searching for a while.
An improvement here would be to include a link to 3.4.2 where idahospiders was defined with the example.
(here's the link: https://lean-lang.org/functional_programming_in_lean/Overloading-and-Type-Classes/Arrays-and-Indexing/#non-empty-list-indexing)
In 3.5.6 ,
idahospidersis used in an Append example , but no mention provided on where it was defined had me searching for a while.An improvement here would be to include a link to 3.4.2 where
idahospiderswas defined with the example.(here's the link: https://lean-lang.org/functional_programming_in_lean/Overloading-and-Type-Classes/Arrays-and-Indexing/#non-empty-list-indexing)