Added thunk-syntax to mimic syntax for products etc (#528)

Author: oisdk

src/Codata/Thunk.agda

@@ -26,6 +26,14 @@ Thunk^R : ∀ {f g r} {F : Size → Set f} {G : Size → Set g}
           (i : Size) (tf : Thunk F ∞) (tg : Thunk G ∞) → Set r
 Thunk^R R i tf tg = Thunk (λ i → R i (tf .force) (tg .force)) i
 
+------------------------------------------------------------------------
+-- Syntax
+
+Thunk-syntax : ∀ {ℓ} → (Size → Set ℓ) → Size → Set ℓ
+Thunk-syntax = Thunk
+
+syntax Thunk-syntax (λ j → e) i = Thunk[ j < i ] e
+
 ------------------------------------------------------------------------
 -- Basic functions.