diff options
| author | Son HO | 2024-06-22 15:07:14 +0200 |
|---|---|---|
| committer | GitHub | 2024-06-22 15:07:14 +0200 |
| commit | 8719c17f1a363c0463d74b90e558b2aaa24645d6 (patch) | |
| tree | 94cd2fb84f10912e76d1d1e8e89d8f9aee948f0c /backends/lean/Base/Primitives/Scalar.lean | |
| parent | 8144c39f4d37aa1fa14a8a061eb7ed60e153fb4c (diff) | |
Do some cleanup in the Lean backend (#257)
Diffstat (limited to '')
| -rw-r--r-- | backends/lean/Base/Primitives/Scalar.lean | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean index 31038e0d..2359c140 100644 --- a/backends/lean/Base/Primitives/Scalar.lean +++ b/backends/lean/Base/Primitives/Scalar.lean @@ -299,7 +299,14 @@ structure Scalar (ty : ScalarTy) where val : Int hmin : Scalar.min ty ≤ val hmax : val ≤ Scalar.max ty -deriving Repr +deriving Repr, BEq, DecidableEq + +instance {ty} : BEq (Scalar ty) where + beq a b := a.val = b.val + +instance {ty} : LawfulBEq (Scalar ty) where + eq_of_beq {a b} := by cases a; cases b; simp[BEq.beq] + rfl {a} := by cases a; simp [BEq.beq] instance (ty : ScalarTy) : CoeOut (Scalar ty) Int where coe := λ v => v.val |