From e932a49469380f8f7bb2e9b58c16b0d5f3e4a65f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?William=20S=C3=B8rensen?= <ws423@cam.ac.uk>
Date: Wed, 26 Jun 2024 14:11:27 +0100
Subject: [PATCH] refactor: transform optimisation step

---
 Qpf/Macro/Comp.lean | 9 +--------
 1 file changed, 1 insertion(+), 8 deletions(-)

diff --git a/Qpf/Macro/Comp.lean b/Qpf/Macro/Comp.lean
index a7336e5..af95e95 100644
--- a/Qpf/Macro/Comp.lean
+++ b/Qpf/Macro/Comp.lean
@@ -194,14 +194,7 @@ partial def handleApp (vars : Vector FVarId arity) (target : Q(Type u))  : TermE
     In such cases, we can directly return `G`, rather than generate a composition of projections.
   -/
 
-  -- O(n²), equivalent to a zipping and would be O(n) and much more readable
-  let is_trivial :=
-    args.length == arity
-    && args.toList.enum.all fun ⟨i, arg⟩ =>
-        arg.isFVar && isLiveVar vars arg.fvarId! && vars'.indexOf arg.fvarId! == i
-  -- Equivalent (?), O(n), and more readable
-  -- TODO: is this really equivalent
-  /- let is_trivial := (args.toList.mapM Expr.fvarId?).any (· == vars') -/
+  let is_trivial := args.toList.mapM Expr.fvarId? == some vars'
 
   if is_trivial then
     trace[QPF] "The application is trivial"