ScopedSnocList: Recalculate argpos in case unelaboration

idris-lang · Feb 21, 2025 · 1c7145f · 1c7145f
1 parent 4a136f2
commit 1c7145f
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/src/TTImp/Unelab.idr b/src/TTImp/Unelab.idr
@@ -81,8 +81,9 @@ mutual
                 | _ => pure Nothing
            let Just argpos = findArgPos treect
                 | _ => pure Nothing
-           if length args == length pargs
-              then mkCase pats argpos args
+           let len = length args
+           if len == length pargs
+              then mkCase pats (len `minus` argpos + 1) args
               else pure Nothing
     where
       -- Need to find the position of the scrutinee to rebuild original