From 3dfa7812f98ed8abc3bfd4e951b1857d239c13b9 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 29 Aug 2024 15:12:54 +1000 Subject: [PATCH] chore: cleanup allowUnsafeReducibility (#5198) --- src/Init/Data/Fin/Lemmas.lean | 3 --- src/Init/Data/Int/DivModLemmas.lean | 3 --- 2 files changed, 6 deletions(-) diff --git a/src/Init/Data/Fin/Lemmas.lean b/src/Init/Data/Fin/Lemmas.lean index 3b8eb7268d..c13120c883 100644 --- a/src/Init/Data/Fin/Lemmas.lean +++ b/src/Init/Data/Fin/Lemmas.lean @@ -11,9 +11,6 @@ import Init.ByCases import Init.Conv import Init.Omega --- Remove after the next stage0 update -set_option allowUnsafeReducibility true - namespace Fin /-- If you actually have an element of `Fin n`, then the `n` is always positive -/ diff --git a/src/Init/Data/Int/DivModLemmas.lean b/src/Init/Data/Int/DivModLemmas.lean index 197888bf00..65fb8dc4ec 100644 --- a/src/Init/Data/Int/DivModLemmas.lean +++ b/src/Init/Data/Int/DivModLemmas.lean @@ -14,9 +14,6 @@ import Init.RCases # Lemmas about integer division needed to bootstrap `omega`. -/ --- Remove after the next stage0 update -set_option allowUnsafeReducibility true - open Nat (succ) namespace Int