chore: add Repr instance for Literal and Key

This commit is contained in:
Leonardo de Moura 2021-07-29 09:34:24 -07:00
parent f10c27dfb7
commit ad216db08d
2 changed files with 2 additions and 2 deletions

View file

@ -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

View file

@ -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)