From e010c10fb9a1e2d88b52a4f6b4a0865448276013 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jul 2023 15:58:38 +0200
Subject: Make the `by inlit` implicit

---
 backends/lean/Base/Primitives.lean | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

(limited to 'backends/lean')

diff --git a/backends/lean/Base/Primitives.lean b/backends/lean/Base/Primitives.lean
index 37abdede..0506f4c0 100644
--- a/backends/lean/Base/Primitives.lean
+++ b/backends/lean/Base/Primitives.lean
@@ -356,8 +356,14 @@ def Scalar.ofIntCore {ty : ScalarTy} (x : Int)
   (hmin : Scalar.min ty ≤ x) (hmax : x ≤ Scalar.max ty) : Scalar ty :=
   { val := x, hmin := hmin, hmax := hmax }
 
+-- Tactic to prove that integers are in bounds
+-- TODO: use this: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/instance.20with.20tactic.20autoparam
+syntax "intlit" : tactic
+macro_rules
+  | `(tactic| intlit) => `(tactic| apply Scalar.bound_suffices; decide)
+
 def Scalar.ofInt {ty : ScalarTy} (x : Int)
-  (h : Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty) : Scalar ty :=
+  (h : Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty := by intlit) : Scalar ty :=
   -- Remark: we initially wrote:
   --  let ⟨ hmin, hmax ⟩ := h
   --  Scalar.ofIntCore x hmin hmax
@@ -573,13 +579,6 @@ instance (ty : ScalarTy) : DecidableEq (Scalar ty) :=
 
 def Scalar.toInt {ty} (n : Scalar ty) : Int := n.val
 
--- Tactic to prove that integers are in bounds
--- TODO: use this: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/instance.20with.20tactic.20autoparam
-syntax "intlit" : tactic
-
-macro_rules
-  | `(tactic| intlit) => `(tactic| apply Scalar.bound_suffices ; decide)
-
 -- -- 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
 -- -- enumerating all of the possible pairs. We remark that Rust has sane semantics
-- 
cgit v1.2.3