Skip to content

Commit 9ae297c

Browse files
committed
[ cleanup ] make short module name private
1 parent 2a2dc29 commit 9ae297c

1 file changed

Lines changed: 3 additions & 2 deletions

File tree

src/Generic/AltSyntax.agda

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -58,8 +58,9 @@ data Raw (A : Set) {I : Set} (d : Desc I) : Size → I → Set where
5858

5959
module ScopeCheck {E I : Set} {d : Desc I} (I-dec : (i j : I) Dec (i ≡ j)) where
6060

61-
M : Set Set
62-
M = (E × String) ⊎_
61+
private
62+
M : Set Set
63+
M = (E × String) ⊎_
6364
open RawMonad (SC.monad (E × String) zero)
6465

6566
varCheck : E × String σ Γ All (κ String) Γ M (Var σ Γ)

0 commit comments

Comments
 (0)