From 04387711deeac00969017bb20dfd8b42a5ac8ec0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Sat, 23 Jul 2022 13:04:36 +0200
Subject: [PATCH] chore: remove unused variables

---
 DocGen4/Output/DocString.lean       | 3 +--
 DocGen4/Process/DefinitionInfo.lean | 5 ++---
 DocGen4/Process/InductiveInfo.lean  | 1 -
 DocGen4/Process/StructureInfo.lean  | 4 ++--
 Main.lean                           | 2 +-
 5 files changed, 6 insertions(+), 9 deletions(-)

diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean
index a501e08..971d066 100644
--- a/DocGen4/Output/DocString.lean
+++ b/DocGen4/Output/DocString.lean
@@ -44,7 +44,7 @@ partial def xmlGetHeadingId (el : Xml.Element) : String :=
   elementToPlainText el |> replaceCharSeq unicodeToDrop "-"
   where
     elementToPlainText el := match el with 
-    | (Element.Element name attrs contents) => 
+    | (Element.Element _ _ contents) => 
       "".intercalate (contents.toList.map contentToPlainText)
     contentToPlainText c := match c with
     | Content.Element el => elementToPlainText el
@@ -138,7 +138,6 @@ def addHeadingAttributes (el : Element) (modifyElement : Element → HtmlM Eleme
 def extendAnchor (el : Element) : HtmlM Element := do
   match el with
   | Element.Element name attrs contents =>
-    let root ← getRoot
     let newAttrs ← match (attrs.find? "href").map extendLink with
     | some href => href.map (attrs.insert "href")
     | none => pure attrs
diff --git a/DocGen4/Process/DefinitionInfo.lean b/DocGen4/Process/DefinitionInfo.lean
index 8a1805a..eb990a5 100644
--- a/DocGen4/Process/DefinitionInfo.lean
+++ b/DocGen4/Process/DefinitionInfo.lean
@@ -14,10 +14,10 @@ open Lean Meta Widget
 
 partial def stripArgs (e : Expr) : Expr :=
   match e.consumeMData with
-  | Expr.lam name type body data =>
+  | Expr.lam name _ body _ =>
     let name := name.eraseMacroScopes
     stripArgs (Expr.instantiate1 body (mkFVar ⟨name⟩))
-  | Expr.forallE name type body data =>
+  | Expr.forallE name _ body _ =>
     let name := name.eraseMacroScopes
     stripArgs (Expr.instantiate1 body (mkFVar ⟨name⟩))
   | _ => e
@@ -28,7 +28,6 @@ def processEq (eq : Name) : MetaM CodeWithInfos := do
   prettyPrintTerm final
 
 def valueToEq (v : DefinitionVal) : MetaM Expr := withLCtx {} {} do
-  let env ← getEnv
   withOptions (tactic.hygienic.set . false) do
     lambdaTelescope v.value fun xs body => do
       let us := v.levelParams.map mkLevelParam
diff --git a/DocGen4/Process/InductiveInfo.lean b/DocGen4/Process/InductiveInfo.lean
index 77c33e5..e2a4db9 100644
--- a/DocGen4/Process/InductiveInfo.lean
+++ b/DocGen4/Process/InductiveInfo.lean
@@ -20,7 +20,6 @@ def getConstructorType (ctor : Name) : MetaM Expr := do
 
 def InductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM InductiveInfo := do
   let info ← Info.ofConstantVal v.toConstantVal
-  let env ← getEnv
   let ctors ← v.ctors.mapM (λ name => do NameInfo.ofTypedName name (←getConstructorType name))
   pure <| InductiveInfo.mk info ctors v.isUnsafe
 
diff --git a/DocGen4/Process/StructureInfo.lean b/DocGen4/Process/StructureInfo.lean
index 256b9b8..ba92593 100644
--- a/DocGen4/Process/StructureInfo.lean
+++ b/DocGen4/Process/StructureInfo.lean
@@ -20,11 +20,11 @@ def dropArgs (type : Expr) (n : Nat) : (Expr × List (Name × Expr)) :=
     let body := body.instantiate1 <| mkFVar ⟨name⟩
     let next := dropArgs body x
     { next with snd := (name, type) :: next.snd}
-  | e, x + 1 => panic! s!"No forallE left"
+  | _e, _x + 1 => panic! s!"No forallE left"
 
 def getFieldTypes (struct : Name) (ctor : ConstructorVal) (parents : Nat) : MetaM (Array NameInfo) := do
   let type := ctor.type
-  let (fieldFunction, params) := dropArgs type (ctor.numParams + parents)
+  let (fieldFunction, _) := dropArgs type (ctor.numParams + parents)
   let (_, fields) := dropArgs fieldFunction (ctor.numFields - parents)
   let mut fieldInfos := #[]
   for (name, type) in fields do
diff --git a/Main.lean b/Main.lean
index 803b444..00606b7 100644
--- a/Main.lean
+++ b/Main.lean
@@ -33,7 +33,7 @@ def runSingleCmd (p : Parsed) : IO UInt32 := do
       pure 0
     | Except.error rc => pure rc
 
-def runIndexCmd (p : Parsed) : IO UInt32 := do
+def runIndexCmd (_p : Parsed) : IO UInt32 := do
   let hierarchy ← Hierarchy.fromDirectory basePath
   let baseConfig := getSimpleBaseContext hierarchy
   htmlOutputIndex baseConfig