Hide Data.Fin.Induction.<-wellFounded in Induction.Nat (#1261)

umazalakain · web-flow · commit 6660e8cc06c6 · 2020-07-23T23:10:41.000+08:00
diff --git a/src/Induction/Nat.agda b/src/Induction/Nat.agda
@@ -10,7 +10,7 @@
 module Induction.Nat where
 
 open import Data.Nat.Induction public
-open import Data.Fin.Induction public
+open import Data.Fin.Induction public hiding (<-wellFounded)
 
 {-# WARNING_ON_IMPORT
 "Induction.Nat was deprecated in v1.1.
