Agda-2.3.2.2: test/interaction/GiveSize.agda

{-# OPTIONS --sized-types #-}
module GiveSize where

postulate Size : Set
{-# BUILTIN SIZE Size #-}

id : Size → Size
id i = {!i!}