diff --git a/SciLean/Core/Meta/GenerateRevCDeriv.lean b/SciLean/Core/Meta/GenerateRevCDeriv.lean index d4b41a3e..bf535518 100644 --- a/SciLean/Core/Meta/GenerateRevCDeriv.lean +++ b/SciLean/Core/Meta/GenerateRevCDeriv.lean @@ -322,6 +322,8 @@ def generateRevCDeriv (constName : Name) (mainNames trailingNames : Array Name) } addDecl (.thmDecl ruleDefInfo) + FTrans.funTransRuleAttr.attr.add ruleDefName (← `(attr|ftrans)) .global + open Lean.Parser.Tactic in def generateHasAdjDiff (constName : Name) (mainNames trailingNames : Array Name) (tac : TSyntax ``tacticSeq) : TermElabM Unit := do diff --git a/test/generate_revCDeriv.lean b/test/generate_revCDeriv.lean index 1d49a930..47193bba 100644 --- a/test/generate_revCDeriv.lean +++ b/test/generate_revCDeriv.lean @@ -59,7 +59,7 @@ info: mymul.arg_xy.revCDeriv_rule_def.{w, u} {K : Type u} [instK : IsROrC K] {W #check mymul.arg_xy.revCDeriv_rule_def -variable +variable {K : Type u} [RealScalar K] {ι : Type v} {κ : Type v'} [EnumType ι] [EnumType κ] @@ -67,7 +67,7 @@ set_default_scalar K def matmul (A : ι → κ → K) (x : κ → K) (i : ι) : K := ∑ j, A i j * x j -#generate_revCDeriv matmul A x by unfold matmul; autodiff; autodiff; +#generate_revCDeriv matmul A x by unfold matmul; autodiff; autodiff #generate_revCDeriv matmul A | i by unfold matmul; autodiff; autodiff #generate_revCDeriv matmul x | i by unfold matmul; autodiff; autodiff @@ -77,4 +77,4 @@ def matmul (A : ι → κ → K) (x : κ → K) (i : ι) : K := ∑ j, A i j * -- need to fix ftrans for this to work -- #generate_revCDeriv matmul A x | i by unfold matmul; autodiff; autodiff - +