remove unneccessary imports

Author: thanhnguyen-aws

Plausible/IR/Action.lean

@@ -1,16 +1,9 @@
 import Lean
-import Std
 import Plausible.IR.Examples
 import Plausible.IR.Extractor
 import Plausible.IR.Prelude
-import Lean.Elab.Deriving.DecEq
-import Lean.Meta.Tactic.Simp.Main
-
-open Lean.Elab.Deriving.DecEq
 open List Nat Array String
 open Lean Elab Command Meta Term LocalContext
-open Lean.Parser.Term
-open Std
 
 namespace Plausible.IR
 

Plausible/IR/Constructor.lean

@@ -1,16 +1,11 @@
 import Lean
-import Std
 import Plausible.IR.Examples
 import Plausible.IR.Extractor
 import Plausible.IR.Prelude
 import Plausible.IR.Prototype
 import Plausible.IR.Action
-import Lean.Elab.Deriving.DecEq
-open Lean.Elab.Deriving.DecEq
 open List Nat Array String
 open Lean Elab Command Meta Term
-open Lean.Parser.Term
-
 
 namespace Plausible.IR
 

Plausible/IR/Extractor.lean

@@ -4,9 +4,6 @@ import Plausible.IR.Examples
 import Plausible.IR.Prelude
 import Plausible.New.Idents
 import Plausible.IR.KeyValueStore
-import Lean.Elab.Deriving.DecEq
-import Batteries.Data.List.Basic
-open Lean.Elab.Deriving.DecEq
 open List Nat Array String
 open Lean Elab Command Meta Term LocalContext
 open Lean.Parser.Term

Plausible/IR/InductiveType.lean

@@ -10,7 +10,6 @@ import Plausible.IR.Constructor
 import Plausible.IR.Backtrack
 open List Nat Array String
 open Lean Elab Command Meta Term
-open Lean.Parser.Term
 open Plausible Gen
 
 

Plausible/IR/Prelude.lean

@@ -1,12 +1,6 @@
 import Lean
-import Std
-import Lean.Elab.Deriving.DecEq
-import Lean.Meta.Tactic.Simp.Main
-
-open Lean.Elab.Deriving.DecEq
 open List Nat Array String
 open Lean Expr Elab Command Meta Term LocalContext
-open Lean.Parser.Term
 open Except
 open Std
 

Plausible/IR/Proof.lean

@@ -331,7 +331,7 @@ mutual
 
 def check_balanced_by_con_1 (h : Nat) (T : Tree) : IO Bool:= do
 {match h , T  with
-| 0 , Tree.Leaf x  =>  return true
+| 0 , Tree.Leaf  =>  return true
 | _ , _  => return false}