Agda Nat exports Unit somehow

[thomas-lamiaux]

I was working on a file and I couldn't get how I was using Unit without importing it. Turned out it was exported by imported Nat. I couldn't figure out where it is imported publicly. I was thinking that this is a bit weird and shouldn't be?

I don't know if there is a link but I have noticed that the Nat Builtin imports the Bool Bultin and I haven't found a reason for that either

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

module Agda.Builtin.Nat where

**open import Agda.Builtin.Bool**

data Nat : Set where
  zero : Nat
  suc  : (n : Nat) → Nat

{-# BUILTIN NATURAL Nat #-}

[mortberg]

I'm confused, what does Agda.Builtin.Nat exporting Bool have to do with Unit?

No matter what it seems weird that Agda.Builtin.Nat imports Agda.Builtin.Bool if it doesn't have to. Seems like an issue for agda (unless there already is an open such issue)

[thomas-lamiaux]

Yes indeed no link.

I find the unit. Nat export Nat.literals that in turn export a some things publicly. Is that normal :

• Base is not self contained
• The export of unit is public ?