bug fix in generate rev/fwdCDeriv

lecopivo · Oct 2, 2023 · f0e24d3 · f0e24d3
1 parent f4612b2
commit f0e24d3
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/SciLean/Core/Meta/GenerateFwdCDeriv.lean b/SciLean/Core/Meta/GenerateFwdCDeriv.lean
@@ -112,7 +112,7 @@ def generateFwdCDeriv (constName : Name) (mainNames trailingNames : Array Name)
       let isDiffRuleName := 
         constName.append lhsData.declSuffix |>.append "IsDifferentiable_rule"
 
-      let xs' := ctx ++ #[W] ++ instW ++ vecInsts ++ args ++ mainArgProps
+      let xs' := ctx ++ #[W] ++ instW ++ vecInsts ++ mergeArgs' mainArgs unusedArgs argKinds ++ mainArgProps
       let isDiffRule ← mkForallFVars xs' isDiff
       let isDiffProof ← mkLambdaFVars xs' isDiffProof
 

diff --git a/SciLean/Core/Meta/GenerateRevCDeriv.lean b/SciLean/Core/Meta/GenerateRevCDeriv.lean
@@ -113,7 +113,7 @@ def generateRevCDeriv (constName : Name) (mainNames trailingNames : Array Name)
       let isDiffRuleName := 
         constName.append lhsData.declSuffix |>.append "HasAdjDiff_rule"
 
-      let xs' := ctx ++ #[W] ++ instW ++ vecInsts ++ args ++ mainArgProps
+      let xs' := ctx ++ #[W] ++ instW ++ vecInsts ++ mergeArgs' mainArgs unusedArgs argKinds ++ mainArgProps
       let isDiffRule ← mkForallFVars xs' isDiff >>= instantiateMVars
       let isDiffProof ← mkLambdaFVars xs' isDiffProof >>= instantiateMVars