consistently use return

jespercockx · Jan 22, 2024 · f842307 · f842307
1 parent e46093e
commit f842307
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/Agda/Core/Typechecker.agda b/src/Agda/Core/Typechecker.agda
@@ -83,15 +83,15 @@ inferPi ctx x su sv u v = do
   tu <- checkType ctx u (TSort su) (sucSort su)
   let wsv = weakenSort (subWeaken subRefl) sv
   tv <- checkType (ctx , x ∶ u) v (TSort wsv) (sucSort wsv)
-  pure $ TSort (funSort su sv) , TyPi tu tv
+  return $ TSort (funSort su sv) , TyPi tu tv
 
 inferTySort : ∀ Γ (s : Sort α) → TCM (Σ[ ty ∈ Type α ] Γ ⊢ TSort s ∶ ty)
 inferTySort ctx (STyp x) = return $ TSort (STyp $ 1 + x) , TyType
 
 inferDef : ∀ Γ (@0 f : name) (p : f ∈ defScope) → TCM (Σ[ ty ∈ Type α ] Γ ⊢ TDef f p ∶ ty)
 inferDef ctx f p = do
   rezz sig ← tcmSignature
-  pure $ weaken subEmpty (getType sig f p) , TyDef p
+  return $ weaken subEmpty (getType sig f p) , TyDef p
 
 checkLambda : ∀ Γ (@0 x : name)
               (u : Term (x ◃ α))