minor clean up of generate revCDeriv

lecopivo · Sep 21, 2023 · 84c7561 · 84c7561
1 parent 72e5a5d
commit 84c7561
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 3 deletions.
diff --git 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
@@ -59,15 +59,15 @@ 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 κ]
 
 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
-
+