open import Agda.Builtin.Nat

thing : Nat
thing =  + 
{-# COMPILE AGDA2LAMBOX thing #-}