From 0ccda640fd39bf95aeb0bcf91e206b14dd6a397f Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 16 Oct 2024 00:12:38 +0100 Subject: [PATCH] feat: characterize `OfScientific.ofScientific` on `Rat` (#990) --- Batteries/Data/Rat/Basic.lean | 3 ++- Batteries/Data/Rat/Lemmas.lean | 6 ++++++ 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/Batteries/Data/Rat/Basic.lean b/Batteries/Data/Rat/Basic.lean index 2032b23ecd..01cbd07859 100644 --- a/Batteries/Data/Rat/Basic.lean +++ b/Batteries/Data/Rat/Basic.lean @@ -112,7 +112,8 @@ def divInt : Int → Int → Rat else (m * 10 ^ e : Nat) -instance : OfScientific Rat where ofScientific := Rat.ofScientific +instance : OfScientific Rat where + ofScientific m s e := Rat.ofScientific (OfNat.ofNat m) s (OfNat.ofNat e) /-- Rational number strictly less than relation, as a `Bool`. -/ protected def blt (a b : Rat) : Bool := diff --git a/Batteries/Data/Rat/Lemmas.lean b/Batteries/Data/Rat/Lemmas.lean index b3c2d49915..844dc7b552 100644 --- a/Batteries/Data/Rat/Lemmas.lean +++ b/Batteries/Data/Rat/Lemmas.lean @@ -332,6 +332,12 @@ theorem ofScientific_def : Rat.ofScientific m s e = if s then mkRat m (10 ^ e) else (m * 10 ^ e : Nat) := by cases s; exact ofScientific_false_def; exact ofScientific_true_def +/-- `Rat.ofScientific` applied to numeric literals is the same as a scientific literal. -/ +@[simp] +theorem ofScientific_ofNat_ofNat : + Rat.ofScientific (no_index (OfNat.ofNat m)) s (no_index (OfNat.ofNat e)) + = OfScientific.ofScientific m s e := rfl + @[simp] theorem intCast_den (a : Int) : (a : Rat).den = 1 := rfl @[simp] theorem intCast_num (a : Int) : (a : Rat).num = a := rfl