From b39e42d7697d03c5d616232670233014c33a92ae Mon Sep 17 00:00:00 2001 From: Yuxiang Date: Fri, 29 Dec 2023 21:01:55 -0800 Subject: [PATCH] Fix 2 more instances of leanprover/fp-lean#137 --- examples/Examples/Classes.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/examples/Examples/Classes.lean b/examples/Examples/Classes.lean index 25fd6f7..ae1d246 100644 --- a/examples/Examples/Classes.lean +++ b/examples/Examples/Classes.lean @@ -781,9 +781,9 @@ stop book declaration book declaration {{{ spiderBoundsChecks }}} -theorem atLeastThreeSpiders : idahoSpiders.inBounds 2 := by simp +theorem atLeastThreeSpiders : idahoSpiders.inBounds 2 := by decide -theorem notSixSpiders : ¬idahoSpiders.inBounds 5 := by simp +theorem notSixSpiders : ¬idahoSpiders.inBounds 5 := by decide stop book declaration namespace Demo