Skip to content

Commit bae8d33

Browse files
authored
Change variable declaration to private (#1256)
1 parent c68e112 commit bae8d33

File tree

1 file changed

+4
-3
lines changed

1 file changed

+4
-3
lines changed

Cubical/Data/List/FinData.agda

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -10,9 +10,10 @@ open import Cubical.Data.Empty as ⊥
1010
open import Cubical.Data.Sigma.Properties
1111
open import Cubical.Data.Nat
1212

13-
variable
14-
: Level
15-
A B : Type ℓ
13+
private
14+
variable
15+
: Level
16+
A B : Type ℓ
1617

1718
-- copy-paste from agda-stdlib
1819
lookup : (xs : List A) Fin (length xs) A

0 commit comments

Comments
 (0)