unicode notation for pi

lecopivo · Nov 27, 2024 · 57c0023 · 57c0023
1 parent b3a74c1
commit 57c0023
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/SciLean/Analysis/Scalar/Basic.lean b/SciLean/Analysis/Scalar/Basic.lean
@@ -10,6 +10,7 @@ import Mathlib.Analysis.Normed.Lp.WithLp
 import Mathlib.MeasureTheory.Measure.MeasureSpaceDef
 
 import SciLean.Analysis.AdjointSpace.Basic
+import SciLean.Analysis.Scalar.Notation
 -- import SciLean.Util.SorryProof
 
 namespace SciLean
@@ -110,6 +111,11 @@ class RealScalar (R : semiOutParam (Type _)) extends Scalar R R, LinearOrder R w
 
 def RealScalar.pi [RealScalar R] : R := RealScalar.acos (-1)
 
+scoped notation "π" => @RealScalar.pi defaultScalar% inferInstance
+
+@[app_unexpander RealScalar.pi] def unexpandPi : Lean.PrettyPrinter.Unexpander
+  | `($_) => `(π)
+
 
 instance {R} [RealScalar R] : MetricSpace (WithLp p R) := (by infer_instance : MetricSpace R)