fixed typo

Antoine-dSG · Jul 24, 2024 · e5c073a · e5c073a
1 parent bcb713e
commit e5c073a
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/FriezePatterns/chapter1.lean b/FriezePatterns/chapter1.lean
@@ -81,5 +81,5 @@ def set_1_to_n (n : Nat) : Set Nat :=
   { i | 1 ≤ i ∧ i ≤ n }
 
 -- The class below looks a bit dubious to me
-class closedFrieze (f : ℕ × ℕ → ℚ) (n : ℕ) extends closedPattern f where
-  positive_n : ∀m, ∀ i ∈ (set_1_to_n n), f (i,m) > 0
+--class closedFrieze (f : ℕ × ℕ → ℚ) (n : ℕ) extends closedPattern f where
+ -- positive_n : ∀m, ∀ i ∈ (set_1_to_n n), f (i,m) > 0