Writing about the feature in the documentation

agda · Dec 23, 2023 · d1325e7 · d1325e7
1 parent 26c1e04
commit d1325e7
Showing 1 changed file with 17 additions and 0 deletions.
diff --git a/docs/source/features.md b/docs/source/features.md
@@ -279,6 +279,23 @@ createRangeCase low high
         False -> Nothing
 ```
 
+## Explicit type singatures
+
+Haskell's `::` syntax for explicit type signatures can be achieved using the `the` function in Haskell.Prim.
+
+Agda:
+```agda
+five : Nat
+five = the (Nat -> Nat) id 5
+{-# COMPILE AGDA2HS five #-}
+```
+
+Haskell:
+```hs
+five :: Natural
+five = (id :: Natural -> Natural) 5
+```
+
 (0-Quantity)=
 ## 0-Quantity Parameters