agda-unused-0.1.0: data/Agda/Builtin/Unit.agda

{-# OPTIONS --without-K --safe --no-universe-polymorphism
            --no-sized-types --no-guardedness --no-subtyping #-}

module Agda.Builtin.Unit where

record ⊤ : Set where
  instance constructor tt

{-# BUILTIN UNIT ⊤ #-}
{-# COMPILE GHC ⊤ = data () (()) #-}