diff --git a/SciLean/Core/Notation/CDeriv.lean b/SciLean/Core/Notation/CDeriv.lean index 54262c10..934f9020 100644 --- a/SciLean/Core/Notation/CDeriv.lean +++ b/SciLean/Core/Notation/CDeriv.lean @@ -10,11 +10,11 @@ syntax diffBinderType := " : " term syntax diffBinderValue := ":=" term (";" term)? syntax diffBinder := ident (diffBinderType <|> diffBinderValue)? -scoped syntax "∂ " term+ : term +scoped syntax "∂ " term:66 : term scoped syntax "∂ " diffBinder ", " term:66 : term scoped syntax "∂ " "(" diffBinder ")" ", " term:66 : term -scoped syntax "∂! " term+ : term +scoped syntax "∂! " term:66 : term scoped syntax "∂! " diffBinder ", " term:66 : term scoped syntax "∂! " "(" diffBinder ")" ", " term:66 : term diff --git a/SciLean/Core/Notation/FwdCDeriv.lean b/SciLean/Core/Notation/FwdCDeriv.lean index 844293b0..7d74d146 100644 --- a/SciLean/Core/Notation/FwdCDeriv.lean +++ b/SciLean/Core/Notation/FwdCDeriv.lean @@ -8,19 +8,19 @@ import SciLean.Core.FunctionTransformations.FwdCDeriv namespace SciLean.NotationOverField -scoped syntax "∂> " term+ : term +scoped syntax "∂> " term:66 : term scoped syntax "∂> " diffBinder ", " term:66 : term scoped syntax "∂> " "(" diffBinder ")" ", " term:66 : term -scoped syntax "∂>! " term+ : term +scoped syntax "∂>! " term:66 : term scoped syntax "∂>! " diffBinder ", " term:66 : term scoped syntax "∂>! " "(" diffBinder ")" ", " term:66 : term open Lean Elab Term Meta in elab_rules : term -| `(∂> $f $xs*) => do +| `(∂> $f $x $xs*) => do let K := mkIdent (← currentFieldName.get) - elabTerm (← `(fwdCDeriv $K $f $xs*)) none + elabTerm (← `(fwdCDeriv $K $f $x $xs*)) none | `(∂> $f) => do let K := mkIdent (← currentFieldName.get) diff --git a/SciLean/Core/Notation/Gradient.lean b/SciLean/Core/Notation/Gradient.lean index 5194089f..56ec9102 100644 --- a/SciLean/Core/Notation/Gradient.lean +++ b/SciLean/Core/Notation/Gradient.lean @@ -5,11 +5,11 @@ import SciLean.Core.Notation.CDeriv namespace SciLean.NotationOverField -scoped syntax (name:=gradNotation1) "∇ " term+ : term +scoped syntax (name:=gradNotation1) "∇ " term:66 : term scoped syntax "∇ " diffBinder ", " term:66 : term scoped syntax "∇ " "(" diffBinder ")" ", " term:66 : term -scoped syntax "∇! " term+ : term +scoped syntax "∇! " term:66 : term scoped syntax "∇! " diffBinder ", " term:66 : term scoped syntax "∇! " "(" diffBinder ")" ", " term:66 : term diff --git a/SciLean/Core/Notation/RevCDeriv.lean b/SciLean/Core/Notation/RevCDeriv.lean index 93527d4f..b690b50e 100644 --- a/SciLean/Core/Notation/RevCDeriv.lean +++ b/SciLean/Core/Notation/RevCDeriv.lean @@ -8,11 +8,11 @@ import SciLean.Core.FunctionTransformations.RevCDeriv namespace SciLean.NotationOverField -scoped syntax "<∂ " term+ : term +scoped syntax "<∂ " term:66 : term scoped syntax "<∂ " diffBinder ", " term:66 : term scoped syntax "<∂ " "(" diffBinder ")" ", " term:66 : term -scoped syntax "<∂! " term+ : term +scoped syntax "<∂! " term:66 : term scoped syntax "<∂! " diffBinder ", " term:66 : term scoped syntax "<∂! " "(" diffBinder ")" ", " term:66 : term diff --git a/test/deriv_notation.lean b/test/deriv_notation.lean index ad68e541..5e452022 100644 --- a/test/deriv_notation.lean +++ b/test/deriv_notation.lean @@ -17,6 +17,10 @@ set_default_scalar K #check ∂ (x:=1), x*x #check ∂ (x:=0.1), x*x #check ∂ (x:=((1:K),(2:K))), (x + x) +#check + let df := ∂ (fun x : K×K => (x.1 + x.2*x.1)) (0,0) + df (0,0) + #check ∂! (fun x : K => x^2) #check ∂! (fun x : K×K => x + x) @@ -24,6 +28,11 @@ set_default_scalar K #check ∂! (x:=((1:K),(2:K))), (x + x) #check ∂! (x:=1), x*x + +#check ∂ (fun x : K => x*x) + = + (fun x => x + x) + variable {X} [Vec K X] (f : X → X) #check ∂ (x:=0), f x @@ -70,7 +79,9 @@ set_default_scalar K #check ∂>! x : K×K, (x.1 + x.2*x.1) #check ∂>! x:=(1:K);2, (x + x*x) - +#check + let a := ∂> (fun x : K×K => (x.1 + x.2*x.1)) + a (0,0) --------------------------------------------------------------------------------