Remove individual autoImplicit (#160)

* Disable autoImplicit globally

* Remove individual autoImplicit lines

Author: pandaman64

correctness/RegexCorrectness/Backtracker/Basic.lean

@@ -5,8 +5,6 @@ import all Regex.Data.BVPos
 import all Regex.Backtracker.Basic
 import Mathlib.Tactic.DepRewrite
 
-set_option autoImplicit false
-
 open Regex.Data (BitMatrix BVPos)
 open String (Pos)
 

correctness/RegexCorrectness/Backtracker/Compile.lean

@@ -4,8 +4,6 @@ import RegexCorrectness.Data.BVPos
 import all RegexCorrectness.Backtracker.Traversal
 import RegexCorrectness.NFA.Semantics
 
-set_option autoImplicit false
-
 open String (Pos)
 open Regex.NFA (EquivUpdate)
 open Regex.Data (CaptureGroups BitMatrix BVPos)

correctness/RegexCorrectness/Backtracker/Correctness.lean

@@ -6,8 +6,6 @@ import all RegexCorrectness.Backtracker.Refinement
 public import RegexCorrectness.Spec
 public import RegexCorrectness.Strategy.Materialize
 
-set_option autoImplicit false
-
 open Regex (NFA)
 open Regex.Data (Expr CaptureGroups)
 open Regex.Strategy (EquivMaterializedUpdate materializeRegexGroups materializeUpdates)

correctness/RegexCorrectness/Backtracker/Path.lean

@@ -3,8 +3,6 @@ module
 import RegexCorrectness.Data.BVPos
 public import RegexCorrectness.NFA.Semantics.Path
 
-set_option autoImplicit false
-
 open String (Pos)
 open Regex.Data (BVPos)
 

correctness/RegexCorrectness/Backtracker/Refinement.lean

@@ -4,8 +4,6 @@ import all RegexCorrectness.Backtracker.Traversal
 import all RegexCorrectness.Strategy.Materialize.Basic
 import RegexCorrectness.Strategy
 
-set_option autoImplicit false
-
 open Regex (NFA)
 open Regex.Data (BitMatrix BVPos)
 open Regex.Strategy (materializeUpdates)

correctness/RegexCorrectness/Backtracker/Traversal/Invariants.lean

@@ -5,8 +5,6 @@ import RegexCorrectness.Data.BVPos
 import all RegexCorrectness.Backtracker.Basic
 import all RegexCorrectness.Backtracker.Path
 
-set_option autoImplicit false
-
 open Regex.Data (BitMatrix BVPos)
 open String (Pos)
 open Regex.NFA (Step)

correctness/RegexCorrectness/Backtracker/Traversal/Lemmas.lean

@@ -2,8 +2,6 @@ module
 
 import all RegexCorrectness.Backtracker.Traversal.Invariants
 
-set_option autoImplicit false
-
 open Regex.Data (BitMatrix BVPos)
 open String (Pos)
 

correctness/RegexCorrectness/Data/BVPos.lean

@@ -4,8 +4,6 @@ import all Regex.Data.BVPos
 public import Regex.Data.BVPos
 import RegexCorrectness.Data.String
 
-set_option autoImplicit false
-
 open String (Pos)
 
 public section

correctness/RegexCorrectness/Data/Expr/Semantics/Backtracking/Equivalence.lean

@@ -3,8 +3,6 @@ module
 public import RegexCorrectness.Data.Expr.Semantics.Backtracking.Basic
 import all RegexCorrectness.Data.Expr.Semantics.Backtracking.Basic
 
-set_option autoImplicit false
-
 open String (Pos)
 
 namespace Regex.Data.Expr.BacktrackingTree

correctness/RegexCorrectness/Data/Expr/Semantics/CaptureGroups.lean

@@ -2,8 +2,6 @@ module
 
 import Regex.Data.Expr.Basic
 
-set_option autoImplicit false
-
 open String (Pos)
 
 public section