chore: cleanup allowUnsafeReducibility (#5198)

2024-08-29 15:12:54 +10:00 · 2024-08-29 15:12:54 +10:00 · 3dfa7812f9
commit 3dfa7812f9
parent 2dd6b2b9c8
2 changed files with 0 additions and 6 deletions
--- 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 -/
--- 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