chore(computability/*FA): remove unnecessary type variables (#5613)

leanprover-community · Jan 4, 2021 · 2300b47 · 2300b47
1 parent 9535f91
commit 2300b47
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/src/computability/DFA.lean b/src/computability/DFA.lean
@@ -27,7 +27,7 @@ structure DFA (α : Type u) (σ : Type v) :=
 
 namespace DFA
 
-variables {α : Type u} {σ σ₁ σ₂ σ₃ : Type v} (M : DFA α σ)
+variables {α : Type u} {σ : Type v} (M : DFA α σ)
 
 instance [inhabited σ] : inhabited (DFA α σ) :=
 ⟨DFA.mk (λ _ _, default σ) (default σ) ∅⟩

diff --git a/src/computability/NFA.lean b/src/computability/NFA.lean
@@ -29,11 +29,11 @@ structure NFA (α : Type u) (σ : Type v) :=
 (start : set σ)
 (accept : set σ)
 
-variables {α : Type u} {σ σ' σ₁ σ₂ σ₃ : Type v} (M : NFA α σ)
+variables {α : Type u} {σ σ' : Type v} (M : NFA α σ)
 
 namespace NFA
 
-instance : inhabited (NFA α σ') := ⟨ NFA.mk (λ _ _, ∅) ∅ ∅ ⟩
+instance : inhabited (NFA α σ) := ⟨ NFA.mk (λ _ _, ∅) ∅ ∅ ⟩
 
 /-- `M.step_set S a` is the union of `M.step s a` for all `s ∈ S`. -/
 def step_set : set σ → α → set σ :=