Merge pull request #79 from leanprover-community/bump_toolchain_to_v4…

….12.0-rc1

chore: bump toolchain to v4.12.0-rc1

ProofWidgets/Demos/Euclidean.lean

@@ -149,7 +149,7 @@ def EuclideanDisplay.rpc (props : PanelWidgetProps) : RequestM (RequestTask Html
         Meta.withLCtx lctx md.localInstances do
           -- Which hypotheses have been selected in the UI,
           -- meaning they should *not* be shown in the display.
-          let mut hiddenLocs : HashSet FVarId := mkHashSet props.selectedLocations.size
+          let mut hiddenLocs : Std.HashSet FVarId := .empty props.selectedLocations.size
           for l in props.selectedLocations do
             match l with
             | ⟨mv, .hyp fv⟩ | ⟨mv, .hypType fv _⟩ =>
@@ -311,7 +311,7 @@ show_panel_widgets [local EuclideanConstructions]
 
 -- Try constructing an equilateral triangle abc
 -- with line segment ab as the base.
-example {a b : Point} (hab : a ≠ b) :
+example {a b : Point} (_hab : a ≠ b) :
     ∃ L M c, onLine a L ∧ onLine b M ∧ onLine c M ∧ onLine c L := by
   -- Place your cursor below.
   -- Shift-click hypotheses in 'Tactic state' to select them.

ProofWidgets/Demos/Venn.lean

@@ -14,7 +14,7 @@ def Set (α : Type u) := α → Prop
 namespace Set
 
 /-- Membership in a set -/
-protected def Mem (a : α) (s : Set α) : Prop :=
+protected def Mem (s : Set α) (a : α) : Prop :=
   s a
 
 instance : Membership α (Set α) :=
@@ -58,14 +58,14 @@ def mkSetDiag (sub : String) (embeds : ExprEmbeds) : MetaM Html := do
 
 def isSetGoal? (hyps : Array LocalDecl) : MetaM (Option Html) := do
   let mut sub := "AutoLabel All\n"
-  let mut sets : HashMap String Expr := .empty
+  let mut sets : Std.HashMap String Expr := .empty
   for assm in hyps do
     let tp ← instantiateMVars assm.type
     if let some (S, T) := isSubsetPred? tp then
       let sS ← toString <$> Lean.Meta.ppExpr S
       let sT ← toString <$> Lean.Meta.ppExpr T
-      let (sets', cS) := sets.insert' sS S
-      let (sets', cT) := sets'.insert' sT T
+      let (cS, sets') := sets.containsThenInsert sS S
+      let (cT, sets') := sets'.containsThenInsert sT T
       sets := sets'
       if !cS then
         sub := sub ++ s!"Set {sS}\n"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.11.0
+leanprover/lean4:v4.12.0-rc1