deprecations

Author: kim-em

ProofWidgets/Demos/Conv.lean

@@ -300,7 +300,7 @@ private def insertAnywhereElse (stx : Syntax) (pathBeforeConvParam : List Nat) (
     | false => List.append (argList.take (pathAfterConv.head! + 1) ) (newNode::(argList.drop (pathAfterConv.head! + 1)))
   let newPath := match entersMerged with
     | true => pathBeforeConvParam ++ (pathAfterConvParam.take 4)
-    | false => pathBeforeConvParam ++ (pathAfterConvParam.take 3) ++ [(pathAfterConvParam.get! 3) + 2]
+    | false => pathBeforeConvParam ++ (pathAfterConvParam.take 3) ++ [pathAfterConvParam[3]! + 2]
 
   t := t.setCur (t.cur.setArgs newArgList.toArray)
   while t.parents.size > 0 do

ProofWidgets/Demos/Dynkin.lean

@@ -81,7 +81,7 @@ def cartanMatrix.E₈ : Matrix (Fin 8) (Fin 8) Int :=
      [ 0,  0,  0, -1,  2, -1,  0,  0],
      [ 0,  0,  0,  0, -1,  2, -1,  0],
      [ 0,  0,  0,  0,  0, -1,  2, -1],
-     [ 0,  0,  0,  0,  0,  0, -1,  2]].get! i |>.get! j
+     [ 0,  0,  0,  0,  0,  0, -1,  2]][i]![j]!
 
 -- Place your cursor here
 #html cartanMatrix.E₈.toHtml

ProofWidgets/Demos/Venn.lean

@@ -1,4 +1,3 @@
-import Lean.Data.HashMap
 import Lean.Elab.Tactic
 import ProofWidgets.Component.Panel.Basic
 import ProofWidgets.Component.PenroseDiagram
@@ -58,7 +57,7 @@ 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 : Std.HashMap String Expr := .empty
+  let mut sets : Std.HashMap String Expr := ∅
   for assm in hyps do
     let tp ← instantiateMVars assm.type
     if let some (S, T) := isSubsetPred? tp then