From f7c09787c4a7457568d3d79d38b45caac4af8772 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 4 Aug 2023 18:19:37 +0200
Subject: Start adding support for Arrays/Slices in the Lean library

---
 backends/lean/Base/Primitives/Scalar.lean | 11 ++---------
 1 file changed, 2 insertions(+), 9 deletions(-)

(limited to 'backends/lean/Base/Primitives/Scalar.lean')

diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 2e5be8bf..ffc969f3 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -787,15 +787,8 @@ instance (ty : ScalarTy) : DecidableEq (Scalar ty) :=
     | isTrue h  => isTrue (Scalar.eq_of_val_eq h)
     | isFalse h => isFalse (Scalar.ne_of_val_ne h)
 
-/- Remark: we can't write the following instance because of restrictions about
-   the type class parameters (`ty` doesn't appear in the return type, which is
-   forbidden):
-
-   ```
-   instance Scalar.cast (ty : ScalarTy) : Coe (Scalar ty) Int where coe := λ v => v.val
-   ```
- -/
-def Scalar.toInt {ty} (n : Scalar ty) : Int := n.val
+instance (ty : ScalarTy) : CoeOut (Scalar ty) Int where
+  coe := λ v => v.val
 
 -- -- We now define a type class that subsumes the various machine integer types, so
 -- -- as to write a concise definition for scalar_cast, rather than exhaustively
-- 
cgit v1.2.3