feat: maps and sets (#460)

Author: david-christiansen

Manual.lean

@@ -193,6 +193,7 @@ LawfulFunctor
 LawfulApplicative
 LawfulMonad
 LawfulBEq
+EquivBEq
 LawfulHashable
 Id
 Thunk
@@ -310,6 +311,35 @@ Eq
 HEq
 Max
 Min
+Std.HashMap
+Std.ExtHashMap
+Std.DHashMap
+Std.ExtDHashMap
+Std.HashSet
+Std.ExtHashSet
+Std.TreeMap
+Std.DTreeMap
+Std.TreeSet
+```
+
+```exceptions
+Std.HashMap.all
+Std.HashMap.equiv_emptyWithCapacity_iff_isEmpty.match_1_1
+Std.HashMap.noConfusionType.withCtor
+Std.HashMap.noConfusionType.withCtorType
+Std.HashMap.«term_~m_»
+```
+
+```exceptions
+Std.DHashMap.equiv_emptyWithCapacity_iff_isEmpty.match_1_1
+Std.DHashMap.insertMany_ind.match_1_1
+Std.DHashMap.isSetoid
+Std.DHashMap.«term_~m_»
+```
+
+```exceptions
+Std.ExtHashMap.noConfusionType.withCtor
+Std.ExtHashMap.noConfusionType.withCtorType
 ```
 
 ```exceptions

Manual/BasicTypes.lean

@@ -21,6 +21,7 @@ import Manual.BasicTypes.Empty
 import Manual.BasicTypes.Products
 import Manual.BasicTypes.Sum
 import Manual.BasicTypes.List
+import Manual.BasicTypes.Maps
 import Manual.BasicTypes.Subtype
 import Manual.BasicTypes.Thunk
 
@@ -315,6 +316,8 @@ Most comparisons on Booleans should be performed using the {inst}`DecidableEq Bo
 
 {include 0 Manual.BasicTypes.Array}
 
+{include 0 Manual.BasicTypes.Maps}
+
 {include 0 Manual.BasicTypes.Subtype}
 
 {include 0 Manual.BasicTypes.Thunk}