From 9ecd354e7114d810bd4a6436ae029e3f7159569b Mon Sep 17 00:00:00 2001
From: lecopivo <skrivantomas@seznam.cz>
Date: Tue, 12 Mar 2024 15:38:13 -0400
Subject: [PATCH] clean up `set_default_scalar` command

---
 SciLean/Core/FunctionSpaces/ContCDiffMap.lean |  8 ++--
 .../Core/FunctionSpaces/ContCDiffMapFD.lean   |  8 ++--
 .../Core/FunctionSpaces/SmoothLinearMap.lean  |  3 ++
 SciLean/Core/Notation/Autodiff.lean           | 18 ---------
 SciLean/Core/Notation/CDeriv.lean             | 38 ++++++++----------
 SciLean/Core/Notation/FwdDeriv.lean           | 22 +++++------
 SciLean/Core/Notation/Gradient.lean           | 34 +++++++---------
 SciLean/Core/Notation/RevCDeriv.lean          | 22 +++++------
 SciLean/Core/NotationOverField.lean           | 23 +++--------
 SciLean/Core/Objects/IsReal.lean              |  3 +-
 .../Core/Objects/SemiInnerProductSpace.lean   | 39 ++++++-------------
 .../Rand/Distributions/WalkOnSpheres.lean     |  4 +-
 12 files changed, 81 insertions(+), 141 deletions(-)
 delete mode 100644 SciLean/Core/Notation/Autodiff.lean

diff --git a/SciLean/Core/FunctionSpaces/ContCDiffMap.lean b/SciLean/Core/FunctionSpaces/ContCDiffMap.lean
index fa4de436..9a7ca583 100644
--- a/SciLean/Core/FunctionSpaces/ContCDiffMap.lean
+++ b/SciLean/Core/FunctionSpaces/ContCDiffMap.lean
@@ -36,10 +36,10 @@ macro X:term:25 " ⟿[" K:term "," n:term "] " Y:term:26 : term =>
   `(ContCDiffMap $K $n $X $Y)
 
 macro X:term:25 " ⟿[" n:term "] " Y:term:26 : term =>
-  `(ContCDiffMap currentScalar% $n $X $Y)
+  `(ContCDiffMap defaultScalar% $n $X $Y)
 
 macro X:term:25 " ⟿ " Y:term:26 : term =>
-  `(ContCDiffMap currentScalar% ∞ $X $Y)
+  `(ContCDiffMap defaultScalar% ∞ $X $Y)
 
 @[app_unexpander ContCDiffMap] def unexpandContCDiffMap : Lean.PrettyPrinter.Unexpander
   | `($(_) $R $n $X $Y) => `($X ⟿[$R,$n] $Y)
@@ -77,11 +77,11 @@ macro "fun " x:funBinder " ⟿[" K:term "," n:term "] " b:term : term =>
 
 open Lean Parser Term
 macro "fun " x:funBinder " ⟿[" n:term "] " b:term : term =>
-  `(ContCDiffMap.mk' currentScalar% $n (fun $x => $b) (by fun_prop (disch:=norm_num; linarith)))
+  `(ContCDiffMap.mk' defaultScalar% $n (fun $x => $b) (by fun_prop (disch:=norm_num; linarith)))
 
 open Lean Parser Term
 macro "fun " x:funBinder " ⟿ " b:term : term =>
-  `(ContCDiffMap.mk' currentScalar% ∞ (fun $x => $b) (by fun_prop (disch:=norm_num; linarith)))
+  `(ContCDiffMap.mk' defaultScalar% ∞ (fun $x => $b) (by fun_prop (disch:=norm_num; linarith)))
 
 @[app_unexpander ContCDiffMap.mk'] def unexpandContCDiffMapMk : Lean.PrettyPrinter.Unexpander
 
diff --git a/SciLean/Core/FunctionSpaces/ContCDiffMapFD.lean b/SciLean/Core/FunctionSpaces/ContCDiffMapFD.lean
index bd709e71..13af5566 100644
--- a/SciLean/Core/FunctionSpaces/ContCDiffMapFD.lean
+++ b/SciLean/Core/FunctionSpaces/ContCDiffMapFD.lean
@@ -37,10 +37,10 @@ macro X:term:25 " ⟿FD[" K:term "," n:term "] " Y:term:26 : term =>
   `(ContCDiffMapFD $K $n $X $Y)
 
 macro X:term:25 " ⟿FD[" n:term "] " Y:term:26 : term =>
-  `(ContCDiffMapFD currentScalar% $n $X $Y)
+  `(ContCDiffMapFD defaultScalar% $n $X $Y)
 
 macro X:term:25 " ⟿FD " Y:term:26 : term =>
-  `(ContCDiffMapFD currentScalar% ∞ $X $Y)
+  `(ContCDiffMapFD defaultScalar% ∞ $X $Y)
 
 @[app_unexpander ContCDiffMapFD] def unexpandContCDiffMapFD : Lean.PrettyPrinter.Unexpander
   | `($(_) $R $n $X $Y) => `($X ⟿FD[$R,$n] $Y)
@@ -63,8 +63,8 @@ macro "fun " x:funBinder " ⟿FD[" K:term "," n:term "] " b:term : term =>
   `(ContCDiffMapFD.mk' $K $n (fun $x => $b) ((fwdDeriv $K fun $x => $b) rewrite_by autodiff /- check that derivative has been eliminated -/) (sorry_proof /- todo: add proof -/) sorry_proof)
 
 
-macro "fun " x:funBinder " ⟿FD[" n:term "] " b:term : term => `(fun $x ⟿FD[currentScalar%, $n] $b)
-macro "fun " x:funBinder " ⟿FD "             b:term : term => `(fun $x ⟿FD[currentScalar%,  ∞] $b)
+macro "fun " x:funBinder " ⟿FD[" n:term "] " b:term : term => `(fun $x ⟿FD[defaultScalar%, $n] $b)
+macro "fun " x:funBinder " ⟿FD "             b:term : term => `(fun $x ⟿FD[defaultScalar%,  ∞] $b)
 
 variable {K n}
 
diff --git a/SciLean/Core/FunctionSpaces/SmoothLinearMap.lean b/SciLean/Core/FunctionSpaces/SmoothLinearMap.lean
index 80f30037..3d7b473f 100644
--- a/SciLean/Core/FunctionSpaces/SmoothLinearMap.lean
+++ b/SciLean/Core/FunctionSpaces/SmoothLinearMap.lean
@@ -28,6 +28,9 @@ instance : FunLike (SmoothLinearMap K X Y) X Y where
 macro X:term:25 " ⊸[" K:term "]" Y:term:26 : term =>
   `(SmoothLinearMap $K $X $Y)
 
+macro X:term:25 " ⊸ " Y:term:26 : term =>
+  `(SmoothLinearMap defaultScalar% $X $Y)
+
 @[fun_prop]
 theorem SmoothLinearMap_apply_right (f : X ⊸[K] Y) : IsSmoothLinearMap K (fun x => f x) := f.2
 
diff --git a/SciLean/Core/Notation/Autodiff.lean b/SciLean/Core/Notation/Autodiff.lean
deleted file mode 100644
index bff6af67..00000000
--- a/SciLean/Core/Notation/Autodiff.lean
+++ /dev/null
@@ -1,18 +0,0 @@
-import SciLean.Core.Notation.Symdiff
-import SciLean.Tactic.LetNormalize
-import SciLean.Tactic.LSimp2.Elab
-import SciLean.Data.Curry
-
-namespace SciLean
-
-open Lean Elab Tactic
-
-macro "autodiff" : conv => do
-  `(conv|
-    (lsimp (config := {failIfUnchanged := false, zeta := false, singlePass := true}) only [cderiv_as_fwdCDeriv, scalarGradient, gradient, scalarCDeriv,revCDerivEval]
-     ftrans only
-     simp (config := {zeta:=false}) only [uncurryN, UncurryN.uncurry, CurryN.curry, curryN]
-     lsimp (config := {failIfUnchanged := false, zeta := false})))
-
-macro "autodiff" : tactic => do
-  `(tactic| conv => autodiff)
diff --git a/SciLean/Core/Notation/CDeriv.lean b/SciLean/Core/Notation/CDeriv.lean
index b28c0672..f17add3d 100644
--- a/SciLean/Core/Notation/CDeriv.lean
+++ b/SciLean/Core/Notation/CDeriv.lean
@@ -5,55 +5,52 @@ import SciLean.Tactic.Autodiff
 -- Notation  -------------------------------------------------------------------
 --------------------------------------------------------------------------------
 
-namespace SciLean.NotationOverField
+namespace SciLean.Notation
 
 syntax diffBinderType  := " : " term
 syntax diffBinderValue := ":=" term (";" term)?
 syntax diffBinder := ident (diffBinderType <|> diffBinderValue)?
 
-scoped syntax "∂ " term:66 : term
-scoped syntax "∂ " diffBinder ", " term:66 : term
-scoped syntax "∂ " "(" diffBinder ")" ", " term:66 : term
+syntax "∂ " term:66 : term
+syntax "∂ " diffBinder ", " term:66 : term
+syntax "∂ " "(" diffBinder ")" ", " term:66 : term
 
-scoped syntax "∂! " term:66 : term
-scoped syntax "∂! " diffBinder ", " term:66 : term
-scoped syntax "∂! " "(" diffBinder ")" ", " term:66 : term
+syntax "∂! " term:66 : term
+syntax "∂! " diffBinder ", " term:66 : term
+syntax "∂! " "(" diffBinder ")" ", " term:66 : term
 
 open Lean Elab Term Meta in
 elab_rules : term
 | `(∂ $f $x $xs*) => do
-  let K := mkIdent (← currentFieldName.get)
-  let KExpr ← elabTerm (← `($K)) none
+  let K ← elabTerm (← `(defaultScalar%)) none
   let X ← inferType (← elabTerm x none)
   let Y ← mkFreshTypeMVar
   let XY ← mkArrow X Y
   -- X might also be infered by the function `f`
   let fExpr ← withoutPostponing <| elabTermEnsuringType f XY false
   let .some (X,_) := (← inferType fExpr).arrow? | return ← throwUnsupportedSyntax
-  if (← isDefEq KExpr X) && xs.size = 0 then
-    elabTerm (← `(scalarCDeriv $K $f $x $xs*)) none false
+  if (← isDefEq K X) && xs.size = 0 then
+    elabTerm (← `(scalarCDeriv defaultScalar% $f $x $xs*)) none false
   else
-    elabTerm (← `(cderiv $K $f $x $xs*)) none false
+    elabTerm (← `(cderiv defaultScalar% $f $x $xs*)) none false
 
 | `(∂ $f) => do
-  let K := mkIdent (← currentFieldName.get)
+  let K ← elabTerm (← `(defaultScalar%)) none
   let X ← mkFreshTypeMVar
   let Y ← mkFreshTypeMVar
   let XY ← mkArrow X Y
-  let KExpr ← elabTerm (← `($K)) none
   let fExpr ← withoutPostponing <| elabTermEnsuringType f XY false
   if let .some (X,_) := (← inferType fExpr).arrow? then
-    if (← isDefEq KExpr X) then
-      elabTerm (← `(scalarCDeriv $K $f)) none false
+    if (← isDefEq K X) then
+      elabTerm (← `(scalarCDeriv defaultScalar% $f)) none false
     else
-      elabTerm (← `(cderiv $K $f)) none false
+      elabTerm (← `(cderiv defaultScalar% $f)) none false
   else
     throwUnsupportedSyntax
 
 -- in this case we do not want to call scalarCDeriv
 | `(∂ $x:ident := $val:term ; $dir:term, $b) => do
-  let K := mkIdent (← currentFieldName.get)
-  elabTerm (← `(cderiv $K (fun $x => $b) $val $dir)) none
+  elabTerm (← `(cderiv defaultScalar% (fun $x => $b) $val $dir)) none
 
 
 macro_rules
@@ -122,6 +119,3 @@ macro_rules
     | _  => `(∂ $f)
 
   | _  => throw ()
-
-
-end NotationOverField
diff --git a/SciLean/Core/Notation/FwdDeriv.lean b/SciLean/Core/Notation/FwdDeriv.lean
index 5e594ae0..0625b357 100644
--- a/SciLean/Core/Notation/FwdDeriv.lean
+++ b/SciLean/Core/Notation/FwdDeriv.lean
@@ -6,26 +6,24 @@ import SciLean.Core.Notation.CDeriv
 -- Notation  -------------------------------------------------------------------
 --------------------------------------------------------------------------------
 
-namespace SciLean.NotationOverField
+namespace SciLean.Notation
 
 
-scoped syntax "∂> " term:66 : term
-scoped syntax "∂> " diffBinder ", " term:66 : term
-scoped syntax "∂> " "(" diffBinder ")" ", " term:66 : term
+syntax "∂> " term:66 : term
+syntax "∂> " diffBinder ", " term:66 : term
+syntax "∂> " "(" diffBinder ")" ", " term:66 : term
 
-scoped syntax "∂>! " term:66 : term
-scoped syntax "∂>! " diffBinder ", " term:66 : term
-scoped syntax "∂>! " "(" diffBinder ")" ", " term:66 : term
+syntax "∂>! " term:66 : term
+syntax "∂>! " diffBinder ", " term:66 : term
+syntax "∂>! " "(" diffBinder ")" ", " term:66 : term
 
 open Lean Elab Term Meta in
 elab_rules : term
 | `(∂> $f $x $xs*) => do
-  let K := mkIdent (← currentFieldName.get)
-  elabTerm (← `(fwdDeriv $K $f $x $xs*)) none
+  elabTerm (← `(fwdDeriv defaultScalar% $f $x $xs*)) none
 
 | `(∂> $f) => do
-  let K := mkIdent (← currentFieldName.get)
-  elabTerm (← `(fwdDeriv $K $f)) none
+  elabTerm (← `(fwdDeriv defaultScalar% $f)) none
 
 
 macro_rules
@@ -67,5 +65,3 @@ macro_rules
     | _  => `(∂> $f)
 
   | _  => throw ()
-
-end NotationOverField
diff --git a/SciLean/Core/Notation/Gradient.lean b/SciLean/Core/Notation/Gradient.lean
index 1343dbc1..806d330f 100644
--- a/SciLean/Core/Notation/Gradient.lean
+++ b/SciLean/Core/Notation/Gradient.lean
@@ -3,22 +3,21 @@ import SciLean.Core.Notation.CDeriv
 import SciLean.Tactic.Autodiff
 
 
-namespace SciLean.NotationOverField
+namespace SciLean.Notation
 
-scoped syntax (name:=gradNotation1) "∇ " term:66 : term
-scoped syntax "∇ " diffBinder ", " term:66 : term
-scoped syntax "∇ " "(" diffBinder ")" ", " term:66 : term
+syntax (name:=gradNotation1) "∇ " term:66 : term
+syntax "∇ " diffBinder ", " term:66 : term
+syntax "∇ " "(" diffBinder ")" ", " term:66 : term
 
-scoped syntax "∇! " term:66 : term
-scoped syntax "∇! " diffBinder ", " term:66 : term
-scoped syntax "∇! " "(" diffBinder ")" ", " term:66 : term
+syntax "∇! " term:66 : term
+syntax "∇! " diffBinder ", " term:66 : term
+syntax "∇! " "(" diffBinder ")" ", " term:66 : term
 
 
 open Lean Elab Term Meta in
 elab_rules (kind:=gradNotation1) : term
 | `(∇ $f $x $xs*) => do
-  let K := mkIdent (← currentFieldName.get)
-  let KExpr ← elabTerm (← `($K)) none
+  let K ← elabTerm (← `(defaultScalar%)) none
   let X ← inferType (← elabTerm x none)
   let Y ← mkFreshTypeMVar
   let XY ← mkArrow X Y
@@ -26,23 +25,22 @@ elab_rules (kind:=gradNotation1) : term
   let fExpr ← withoutPostponing <| elabTermEnsuringType f XY false
   let .some (_,Y) := (← inferType fExpr).arrow?
     | return ← throwUnsupportedSyntax
-  if (← isDefEq KExpr Y) then
-    elabTerm (← `(scalarGradient $K $f $x $xs*)) none false
+  if (← isDefEq K Y) then
+    elabTerm (← `(scalarGradient defaultScalar% $f $x $xs*)) none false
   else
-    elabTerm (← `(gradient $K $f $x $xs*)) none false
+    elabTerm (← `(gradient defaultScalar% $f $x $xs*)) none false
 
 | `(∇ $f) => do
-  let K := mkIdent (← currentFieldName.get)
+  let K ← elabTerm (← `(defaultScalar%)) none
   let X ← mkFreshTypeMVar
   let Y ← mkFreshTypeMVar
   let XY ← mkArrow X Y
-  let KExpr ← elabTerm (← `($K)) none
   let fExpr ← withoutPostponing <| elabTermEnsuringType f XY false
   if let .some (_,Y) := (← inferType fExpr).arrow? then
-    if (← isDefEq KExpr Y) then
-      elabTerm (← `(scalarGradient $K $f)) none false
+    if (← isDefEq K Y) then
+      elabTerm (← `(scalarGradient defaultScalar% $f)) none false
     else
-      elabTerm (← `(gradient $K $f)) none false
+      elabTerm (← `(gradient defaultScalar% $f)) none false
   else
     throwUnsupportedSyntax
 
@@ -107,5 +105,3 @@ macro_rules
     | _  => `(∇ $f)
 
   | _  => throw ()
-
-end SciLean.NotationOverField
diff --git a/SciLean/Core/Notation/RevCDeriv.lean b/SciLean/Core/Notation/RevCDeriv.lean
index 5167957e..945d60d1 100644
--- a/SciLean/Core/Notation/RevCDeriv.lean
+++ b/SciLean/Core/Notation/RevCDeriv.lean
@@ -6,24 +6,22 @@ import SciLean.Core.FunctionTransformations.RevDeriv
 -- Notation  -------------------------------------------------------------------
 --------------------------------------------------------------------------------
 
-namespace SciLean.NotationOverField
+namespace SciLean.Notation
 
-scoped syntax "<∂ " term:66 : term
-scoped syntax "<∂ " diffBinder ", " term:66 : term
-scoped syntax "<∂ " "(" diffBinder ")" ", " term:66 : term
+syntax "<∂ " term:66 : term
+syntax "<∂ " diffBinder ", " term:66 : term
+syntax "<∂ " "(" diffBinder ")" ", " term:66 : term
 
-scoped syntax "<∂! " term:66 : term
-scoped syntax "<∂! " diffBinder ", " term:66 : term
-scoped syntax "<∂! " "(" diffBinder ")" ", " term:66 : term
+syntax "<∂! " term:66 : term
+syntax "<∂! " diffBinder ", " term:66 : term
+syntax "<∂! " "(" diffBinder ")" ", " term:66 : term
 
 open Lean Elab Term Meta in
 elab_rules : term
 | `(<∂ $f $xs*) => do
-  let K := mkIdent (← currentFieldName.get)
-  elabTerm (← `(revDeriv $K $f $xs*)) none
+  elabTerm (← `(revDeriv defaultScalar% $f $xs*)) none
 | `(<∂ $f) => do
-  let K := mkIdent (← currentFieldName.get)
-  elabTerm (← `(revDeriv $K $f)) none
+  elabTerm (← `(revDeriv defaultScalar% $f)) none
 -- | `(<∂ $x:ident := $val:term ; $codir:term, $b) => do
 --   let K := mkIdent (← currentFieldName.get)
 --   elabTerm (← `(revDerivEval $K (fun $x => $b) $val $codir)) none
@@ -69,5 +67,3 @@ macro_rules
 --     | _  => throw ()
 
 --   | _ => throw ()
-
-end NotationOverField
diff --git a/SciLean/Core/NotationOverField.lean b/SciLean/Core/NotationOverField.lean
index 13f04140..822cb5a0 100644
--- a/SciLean/Core/NotationOverField.lean
+++ b/SciLean/Core/NotationOverField.lean
@@ -4,31 +4,20 @@ open Lean Elab Command Term
 namespace SciLean
 namespace NotationOverField
 
+syntax "defaultScalar%" : term
 
-initialize currentFieldName : IO.Ref Name ← IO.mkRef default
-
-elab "open_notation_over_field" K:ident : command => do
-  currentFieldName.set K.getId
-  Lean.Elab.Command.elabCommand <| ←
-   `(open SciLean.NotationOverField)
-
-macro "set_default_scalar " K:ident : command => `(open_notation_over_field $K)
-
-
-syntax "currentScalar%" : term
-
-macro_rules | `(currentScalar%) => Lean.Macro.throwError "\
+macro_rules | `(defaultScalar%) => Lean.Macro.throwError "\
   This expression is using notation requiring to know the default scalar type. \
   To set it, add this command somewhere to your file \
-  \n\n set_current_scalar R\
+  \n\n set_default_scalar R\
   \n\n\
   where R is the desired scalar, usually ℝ or Float.\n\n\
   If you want to write code that is agnostic about the particular scalar \
   type then introduce a generic type R with instance of `RealScalar R` \
   \n\n  variable {R : Type _} [RealScalar R]\
-  \n  set_current_scalar R\
+  \n  set_default_scalar R\
   \n\n\
   TODO: write a doc page about writing field polymorphic code and add a link here"
 
-macro "set_current_scalar" r:term : command =>
-  `(local macro_rules | `(currentScalar%) => `($r))
+macro "set_default_scalar" r:term : command =>
+  `(local macro_rules | `(defaultScalar%) => `($r))
diff --git a/SciLean/Core/Objects/IsReal.lean b/SciLean/Core/Objects/IsReal.lean
index 5e61d4e3..8933b6d1 100644
--- a/SciLean/Core/Objects/IsReal.lean
+++ b/SciLean/Core/Objects/IsReal.lean
@@ -88,8 +88,7 @@ open Lean Elab Term
   WARRNING: This is override for normal norm notation that provides computable version of norm if available.
 -/
 scoped elab (priority := high) "‖" x:term "‖" : term => do
-  let K := mkIdent (← currentFieldName.get)
-  elabTerm (← `(cnorm (R:=$K) $x)) none
+  elabTerm (← `(cnorm (R:=defaultScalar%) $x)) none
   -- TODO: fall back to normal norm if
 
 end NotationOverField
diff --git a/SciLean/Core/Objects/SemiInnerProductSpace.lean b/SciLean/Core/Objects/SemiInnerProductSpace.lean
index e2ce5388..0511eb0d 100644
--- a/SciLean/Core/Objects/SemiInnerProductSpace.lean
+++ b/SciLean/Core/Objects/SemiInnerProductSpace.lean
@@ -18,10 +18,21 @@ instance [Inner K X] : Norm2 K X where
   norm2 x := Inner.inner x x
 
 notation "‖" x "‖₂²[" K "]" => @Norm2.norm2 K _ _ x
+macro "‖" x:term "‖₂²" : term => `(@Norm2.norm2 defaultScalar% _ _ $x)
+
+@[app_unexpander Norm2.norm2] def unexpandNorm2 : Lean.PrettyPrinter.Unexpander
+  | `($(_) $x) => `(‖ $x ‖₂²)
+  | _ => throw ()
+
 
 def norm₂ (K : Type _) {R X : Type _} [Scalar R K] [Norm2 K X] (x : X) : K := Scalar.sqrt (Norm2.norm2 x)
 
 notation "‖" x "‖₂[" K "]" => norm₂ K x
+macro "‖" x:term "‖₂" : term => `(norm₂ defaultScalar% $x)
+
+@[app_unexpander norm₂] def unexpandNorm₂ : Lean.PrettyPrinter.Unexpander
+  | `($(_) K $x) => `(‖ $x ‖₂)
+  | _ => throw ()
 
 @[simp]
 theorem norm₂_squared_nat {R K X : Type _} [Scalar R K] [Norm2 K X] (x : X)
@@ -34,38 +45,12 @@ theorem norm₂_squared {R K X : Type _} [Scalar R K] [Norm2 K X] (x : X)
 section Inner
 
 notation "⟪" x ", " y "⟫[" K "]" => @Inner.inner K _ _ x y
-
-namespace NotationOverField
-
-scoped elab "‖" x:term "‖₂²" : term => do
-  let fieldName ← currentFieldName.get
-  let K := Lean.mkIdent fieldName
-  Lean.Elab.Term.elabTerm (← `(@Norm2.norm2 $K _ _ $x)) none
-
-@[app_unexpander Norm2.norm2] def unexpandNorm2 : Lean.PrettyPrinter.Unexpander
-  | `($(_) $x) => `(‖ $x ‖₂²)
-  | _ => throw ()
-
-scoped elab "‖" x:term "‖₂" : term => do
-  let fieldName ← currentFieldName.get
-  let K := Lean.mkIdent fieldName
-  Lean.Elab.Term.elabTerm (← `(norm₂ $K $x)) none
-
-@[app_unexpander norm₂] def unexpandNorm₂ : Lean.PrettyPrinter.Unexpander
-  | `($(_) K $x) => `(‖ $x ‖₂)
-  | _ => throw ()
-
-scoped elab "⟪" x:term ", " y:term "⟫" : term => do
-  let fieldName ← currentFieldName.get
-  let K := Lean.mkIdent fieldName
-  Lean.Elab.Term.elabTerm (← `(@Inner.inner $K _ _ $x $y)) none
+macro "⟪" x:term ", " y:term "⟫" : term => `(@Inner.inner defaultScalar% _ _ $x $y)
 
 @[app_unexpander Inner.inner] def unexpandInner : Lean.PrettyPrinter.Unexpander
   | `($(_) $x $y) => `(⟪$x, $y⟫)
   | _ => throw ()
 
-end NotationOverField
-
 
 instance (K X Y) [AddCommMonoid K] [Inner K X] [Inner K Y] : Inner K (X × Y) where
   inner := λ (x,y) (x',y') => ⟪x,x'⟫[K] + ⟪y,y'⟫[K]
diff --git a/SciLean/Core/Rand/Distributions/WalkOnSpheres.lean b/SciLean/Core/Rand/Distributions/WalkOnSpheres.lean
index ebcb0152..720216e3 100644
--- a/SciLean/Core/Rand/Distributions/WalkOnSpheres.lean
+++ b/SciLean/Core/Rand/Distributions/WalkOnSpheres.lean
@@ -98,7 +98,7 @@ def harmonicRec.arg_x.fwdDeriv_randApprox (n : ℕ)
   pure (f' x dx)
 
 
-set_current_scalar Float
+set_default_scalar Float
 
 
 noncomputable
@@ -113,7 +113,7 @@ theorem harmonicRec'_CDifferentiable (n : ℕ) :
     CDifferentiable Float (fun (w : (Vec3 ⟿FD Float)×(Vec3 ⟿FD Y)×Vec3) => harmonicRec' n w.1 w.2.1 w.2.2) := by
   induction n <;> (simp[harmonicRec']; fun_prop)
 
-set_option profiler true
+
 -- set_option trace.Meta.Tactic.fun_trans true in
 -- set_option trace.Meta.Tactic.fun_prop true in
 noncomputable