fix euclid-mullin

UniMath · Oct 24, 2024 · 4570923 · 4570923
1 parent ffdf33c
commit 4570923
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/src/elementary-number-theory/euclid-mullin-sequence.lagda.md b/src/elementary-number-theory/euclid-mullin-sequence.lagda.md
@@ -45,16 +45,16 @@ previous entries in the Euclid–Mullin sequence plus one.
 ### The Euclid–Mullin sequence
 
 ```agda
-{-# TERMINATING #-}
-
 euclid-mullin-ℕ : ℕ → ℕ
 euclid-mullin-ℕ =
   strong-rec-ℕ
     ( 2)
     ( λ n f →
       nat-least-nontrivial-divisor-ℕ'
         ( succ-ℕ
-          ( Π-ℕ (succ-ℕ n) (λ i → euclid-mullin-ℕ (nat-Fin (succ-ℕ n) i)))))
+          ( Π-ℕ
+            ( succ-ℕ n)
+            ( λ i → f (nat-Fin (succ-ℕ n) i) (upper-bound-nat-Fin n i)))))
 
 compute-euclid-mullin-0-ℕ : euclid-mullin-ℕ 0 ＝ 2
 compute-euclid-mullin-0-ℕ = refl