revert notation changes

lecopivo · Apr 9, 2024 · 4a91f8f · 4a91f8f
1 parent f2c68ca
commit 4a91f8f
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/SciLean/Core/Notation/CDeriv.lean b/SciLean/Core/Notation/CDeriv.lean
@@ -57,7 +57,7 @@ macro_rules
 | `(∂ $x:term, $b) => `(∂ (fun $x => $b))
 | `(∂ $x:term := $val:term, $b) => `(∂ (fun $x => $b) $val)
 | `(∂ $x:term : $type:term, $b) => `(∂ fun $x : $type => $b)
--- | `(∂ ($b:diffBinder), $f)       => `(∂ $b, $f)
+| `(∂ ($b:diffBinder), $f)       => `(∂ $b, $f)
 
 macro_rules
 -- in some cases it is still necessary to call fun_trans multiple times

diff --git a/SciLean/Core/Notation/FwdDeriv.lean b/SciLean/Core/Notation/FwdDeriv.lean
@@ -31,7 +31,7 @@ macro_rules
 | `(∂> $x:term := $val:term, $b) => `(∂> (fun $x => $b) $val)
 | `(∂> $x:term : $type:term, $b) => `(∂> fun $x : $type => $b)
 | `(∂> $x:term := $val:term ; $dir:term, $b) => `(∂> (fun $x => $b) $val $dir)
--- | `(∂> ($b:diffBinder), $f)       => `(∂> $b, $f)
+| `(∂> ($b:diffBinder), $f)       => `(∂> $b, $f)
 
 
 macro_rules