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)