Skip to content

Commit b9386f3

Browse files
authored
Remove the public export of factorial from LehmerCode.agda
1 parent 630f3be commit b9386f3

File tree

1 file changed

+0
-1
lines changed

1 file changed

+0
-1
lines changed

Cubical/Data/Fin/LehmerCode.agda

-1
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,6 @@ open import Cubical.Relation.Nullary
2222
open import Cubical.Data.Unit as ⊤
2323
open import Cubical.Data.Empty as ⊥
2424
open import Cubical.Data.Nat
25-
open import Cubical.Data.Nat.Properties using (factorial) public
2625
open import Cubical.Data.Nat.Order
2726
open import Cubical.Data.Fin.Base as F
2827
open import Cubical.Data.Fin.Properties

0 commit comments

Comments
 (0)