chore: drop unused 'reducible' lemma (#322)

opencompl · May 21, 2024 · 1a42909 · 1a42909
1 parent 4062b06
commit 1a42909
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/SSA/Core/ErasedContext.lean b/SSA/Core/ErasedContext.lean
@@ -11,7 +11,6 @@ import SSA.Core.HVector
   Intuitively, each `b : β` represents a Lean `Type`, but using `β` instead of `Type` directly
   avoids a universe bump
 -/
-@[reducible]
 class TyDenote (β : Type) : Type 1 where
   toType : β → Type
 open TyDenote (toType) /- make toType publically visible in module. -/