chore: instMembershipListLanguage -> Language.instMembershipList

opencompl · Dec 26, 2024 · 42d5714 · 42d5714
1 parent 18a73cf
commit 42d5714
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/SSA/Experimental/Bits/AutoStructs/FormulaToAuto.lean b/SSA/Experimental/Bits/AutoStructs/FormulaToAuto.lean
@@ -19,9 +19,9 @@ import SSA.Experimental.Bits.AutoStructs.NFA'
 open AutoStructs
 open Mathlib
 
+set_option pp.explicit true in
 @[simp] theorem Language.mem_setOf_eq {x : List α} {p : List α → Prop} :
-    @Membership.mem (List α) (Language α) instMembershipListLanguage {y | p y} x = p x := by
-  rfl
+    @Membership.mem (List α) (Language α) Language.instMembershipList {y | p y} x = p x := rfl
 
 @[simp] theorem Language.trivial : x ∈ (⊤ : Language α) := by trivial