From 487143705ad7bcadb5158122ade7d11eec02fd26 Mon Sep 17 00:00:00 2001
From: Marcin Grzybowski <marcinjangrzybowski@gmail.com>
Date: Wed, 28 Aug 2024 19:45:09 +0200
Subject: [PATCH] fixing  name clash

---
 Cubical/Data/List/Properties.agda                       | 4 ++--
 Cubical/Tactics/PathSolver/MonoidalSolver/PathEval.agda | 4 ++--
 Cubical/Tactics/PathSolver/NSolver/NSolver.agda         | 6 +++---
 Cubical/Tactics/Reflection/Utilities.agda               | 2 +-
 4 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/Cubical/Data/List/Properties.agda b/Cubical/Data/List/Properties.agda
index 6ce8c9214..79dac3890 100644
--- a/Cubical/Data/List/Properties.agda
+++ b/Cubical/Data/List/Properties.agda
@@ -341,8 +341,8 @@ lookupAlways a [] _ = a
 lookupAlways _ (x ∷ _) zero = x
 lookupAlways a (x ∷ xs) (suc k) = lookupAlways a xs k
 
-lookup : List A → ℕ → Maybe A
-lookup = lookupAlways nothing ∘S map just
+lookupMb : List A → ℕ → Maybe A
+lookupMb = lookupAlways nothing ∘S map just
 
 rot : List A → List A
 rot [] = []
diff --git a/Cubical/Tactics/PathSolver/MonoidalSolver/PathEval.agda b/Cubical/Tactics/PathSolver/MonoidalSolver/PathEval.agda
index 9cf73539b..6e3c81dcb 100644
--- a/Cubical/Tactics/PathSolver/MonoidalSolver/PathEval.agda
+++ b/Cubical/Tactics/PathSolver/MonoidalSolver/PathEval.agda
@@ -294,7 +294,7 @@ fill-flatten' = hTop ∘S atVarOrConOrDefMmp
  fill-offsetPa' : ℕ → List (R.Arg R.Term) → List (R.Arg R.Term)
  fill-offsetPa' n xs =
   let hd = fromJust-def (varg (R.lit (R.string "fatal in PathEval - offsetPa'")))
-            (lookup xs zero)
+            (lookupMb xs zero)
       hs* = mapArg (dropFillWraps headFW) hd
       hd' = mapArg
              (replaceVarWithCon (λ { zero → just (quote i0) ; _ → nothing })) hs*
@@ -310,7 +310,7 @@ fill-flatten' = hTop ∘S atVarOrConOrDefMmp
 
  hTop : List R.Term → List R.Term
  hTop = L.map (Mb.fromJust-def ( (R.lit (R.string "imposible in fill-flatten'")) )
-   ∘S map-Maybe (unArg) ∘S flip lookup zero) ∘S h ∘S [_] ∘S L.map varg
+   ∘S map-Maybe (unArg) ∘S flip lookupMb zero) ∘S h ∘S [_] ∘S L.map varg
 
  df : ℕ →
         R.Name →
diff --git a/Cubical/Tactics/PathSolver/NSolver/NSolver.agda b/Cubical/Tactics/PathSolver/NSolver/NSolver.agda
index 8e168eb34..4097b9eb7 100644
--- a/Cubical/Tactics/PathSolver/NSolver/NSolver.agda
+++ b/Cubical/Tactics/PathSolver/NSolver/NSolver.agda
@@ -309,9 +309,9 @@ module _ (ty : R.Type) where
    fcs0₀ ← Mb.rec (R.typeError [ "imposible" ]ₑ)
               (λ y → mapM (λ k → (getVert 100 (replaceAt k true v0)) (fst y)
                             <|> fail ("fcs1 fail" ∷nl [ k ]ₑ))  (range dim))
-             (lookup fcs0 0)
+             (lookupMb fcs0 0)
    fcs0₁ ← Mb.rec (R.typeError [ "imposible" ]ₑ)
-     (getVert 100 (replaceAt (predℕ dim) true v0) ∘S fst) (lookup fcs0 1)
+     (getVert 100 (replaceAt (predℕ dim) true v0) ∘S fst) (lookupMb fcs0 1)
 
    fcs1 ← mapM (idfun _)
            (zipWith (markVertSnd 100 dim) (fcs0₁ ∷ fcs0₀) ((snd ∘S snd) <$> xs))
@@ -480,7 +480,7 @@ solvePathsSolver goal = R.withReduceDefs (false , doNotReduceInPathSolver) do
  R.debugPrint "solvePaths" 0 $ [ "solvePaths - matchNCube done" ]ₑ
  let dim = length fcs
 
- (t0 , _) ← Mb.rec (R.typeError [ "imposible in solvePaths''" ]ₑ) pure (lookup fcs zero)
+ (t0 , _) ← Mb.rec (R.typeError [ "imposible in solvePaths''" ]ₑ) pure (lookupMb fcs zero)
 
  cuFcs ← ((zipWithIndex <$> quoteBd bdTM
             -- <|> R.typeError [ "quoteBd - failed" ]ₑ
diff --git a/Cubical/Tactics/Reflection/Utilities.agda b/Cubical/Tactics/Reflection/Utilities.agda
index 3cef6c2ec..c2395ea1d 100644
--- a/Cubical/Tactics/Reflection/Utilities.agda
+++ b/Cubical/Tactics/Reflection/Utilities.agda
@@ -387,7 +387,7 @@ replaceVarWithTerm f =
 
 
 substTms : List Term → Term →  Term
-substTms xs = dropVars.rv (length xs) zero ∘S replaceVarWithTerm (lookup (map (liftVarsFrom (length xs) 0) xs))
+substTms xs = dropVars.rv (length xs) zero ∘S replaceVarWithTerm (lookupMb (map (liftVarsFrom (length xs) 0) xs))
 
 replaceAtTrm : ℕ → Term → Term → Term
 replaceAtTrm k t =