{-# OPTIONS --sized-types #-}

module Haskell.Prim.Thunk where

open import Agda.Builtin.Size public

open import Haskell.Prim

record Thunk {} (a : @0 Size  Set ) (@0 i : Size) : Set  where
  constructor delay
  coinductive
  field force : {j : Size< i}  a j
open Thunk public

{-# COMPILE AGDA2HS Thunk unboxed #-}