From 278d47c77270664ef29715faab467feac8a0f446 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 4 Feb 2021 20:40:05 -0800 Subject: [PATCH] chore: add `Repr` instance for `TransparencyMode` --- src/Lean/Meta/TransparencyMode.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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