From b744e862f4e59fd9c77ffae7cd9bf97acadd039a Mon Sep 17 00:00:00 2001 From: mehbark Date: Tue, 8 Apr 2025 22:43:43 -0400 Subject: [PATCH] BadInfinities: fix no_int_infinity --- SimpleCounterexamples/BadInfinities.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/SimpleCounterexamples/BadInfinities.lean b/SimpleCounterexamples/BadInfinities.lean index 59fe492..daf035a 100644 --- a/SimpleCounterexamples/BadInfinities.lean +++ b/SimpleCounterexamples/BadInfinities.lean @@ -11,7 +11,7 @@ theorem lt_irrefl_imp_no_infinity theorem no_nat_infinity : ¬HasInfinity Nat := lt_irrefl_imp_no_infinity Nat Nat.lt_irrefl -theorem no_int_infinity : ¬HasInfinity Nat := - lt_irrefl_imp_no_infinity Nat Nat.lt_irrefl +theorem no_int_infinity : ¬HasInfinity Int := + lt_irrefl_imp_no_infinity Int Int.lt_irrefl -- it's… not difficult to see the pattern