diff --git a/src/Lean/Meta/TransparencyMode.lean b/src/Lean/Meta/TransparencyMode.lean index 44ebf8acaa..4d07fc9ddb 100644 --- a/src/Lean/Meta/TransparencyMode.lean +++ b/src/Lean/Meta/TransparencyMode.lean @@ -7,7 +7,7 @@ namespace Lean.Meta inductive TransparencyMode where | all | default | reducible | instances - deriving Inhabited, BEq + deriving Inhabited, BEq, Repr namespace TransparencyMode