diff options
Diffstat (limited to 'backends/lean')
| -rw-r--r-- | backends/lean/Base/Primitives.lean | 15 |
1 files changed, 7 insertions, 8 deletions
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 |