fix tyApp' comilation

jespercockx · Oct 28, 2024 · da40554 · da40554
1 parent 0a86b61
commit da40554
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/src/Agda/Core/Typing.agda b/src/Agda/Core/Typing.agda
@@ -277,6 +277,7 @@ tyApp' : {@0 Γ : Context α} {b : Type α} {c : Type (x ◃ α)} {@0 r : Rezz
   ------------------------------------
   → Γ ⊢ TApp u v ∶ substTop {t = λ (@0 v) → Type v} r v c
 tyApp' {r = rezz α} tyu tyv = TyApp tyu tyv
+{-# COMPILE AGDA2HS tyApp' #-}
 
 tyCase' : {@0 Γ : Context α} 
   {d : NameIn dataScope}