From ad216db08d5b1d318fa453749f3a41a686dbf474 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 29 Jul 2021 09:34:24 -0700 Subject: [PATCH] chore: add `Repr` instance for `Literal` and `Key` --- src/Lean/Expr.lean | 2 +- src/Lean/Meta/DiscrTreeTypes.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index 8dc107aac0..df80083a6c 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean @@ -11,7 +11,7 @@ namespace Lean inductive Literal where | natVal (val : Nat) | strVal (val : String) - deriving Inhabited, BEq + deriving Inhabited, BEq, Repr protected def Literal.hash : Literal → UInt64 | Literal.natVal v => hash v diff --git a/src/Lean/Meta/DiscrTreeTypes.lean b/src/Lean/Meta/DiscrTreeTypes.lean index 460991be47..2910131431 100644 --- a/src/Lean/Meta/DiscrTreeTypes.lean +++ b/src/Lean/Meta/DiscrTreeTypes.lean @@ -18,7 +18,7 @@ inductive Key where | star : Key | other : Key | arrow : Key - deriving Inhabited, BEq + deriving Inhabited, BEq, Repr protected def Key.hash : Key → UInt64 | Key.const n a => mixHash 5237 $ mixHash (hash n) (hash a)