feat: section intro

Also note that it fixes #64.
leanprover · Oct 31, 2024 · 46e33e6 · 46e33e6
1 parent 0ff26d7
commit 46e33e6
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 6 deletions.
diff --git a/Manual/Language/Classes.lean b/Manual/Language/Classes.lean
@@ -623,12 +623,6 @@ instance $p?
 tag := "deriving-instances"
 %%%
 
-::: planned 64
-This section will specify syntax of `deriving` clauses and list the valid places where they may occur.
-It will also describe `deriving instance`.
-It will list the deriving handlers that ship with Lean by default.
-:::
-
 
 {include 2 Manual.Language.Classes.DerivingHandlers}
 

diff --git a/Manual/Language/Classes/BasicClasses.lean b/Manual/Language/Classes/BasicClasses.lean
@@ -18,6 +18,8 @@ open Verso.Genre.Manual
 tag := "basic-classes"
 %%%
 
+Many Lean type classes exist in order to allow built-in notations such as addition or array indexing to be overloaded.
+
 # Boolean Equality Tests
 
 {docstring BEq}