Simplify iteration in kvar encoding

flux-rs · Feb 5, 2025 · cd33967 · cd33967
1 parent fc342c7
commit cd33967
Showing 1 changed file with 2 additions and 3 deletions.
diff --git a/crates/flux-infer/src/fixpoint_encoding.rs b/crates/flux-infer/src/fixpoint_encoding.rs
@@ -607,7 +607,7 @@ where
             .iter()
             .enumerate()
             .map(|(i, kvid)| {
-                let args = all_args.iter().skip(kvids.len() - i - 1).copied().collect();
+                let args = all_args[i..].to_vec();
                 fixpoint::Pred::KVar(*kvid, args)
             })
             .collect_vec();
@@ -675,7 +675,7 @@ impl KVarEncodingCtxt {
                     let n = usize::max(decl.self_args, 1);
                     (0..n)
                         .map(|i| {
-                            let sorts = all_args.iter().skip(n - i - 1).cloned().collect();
+                            let sorts = all_args[i..].to_vec();
                             self.kvars.push(FixpointKVar::new(sorts, kvid))
                         })
                         .collect_vec()
@@ -743,7 +743,6 @@ impl LocalVarEnv {
     }
 }
 
-#[derive(Clone)]
 struct ConstInfo {
     name: fixpoint::GlobalVar,
     sort: fixpoint::Sort,