{-# OPTIONS --level-universe #-}
open import Agda.Builtin.Nat using (Nat)

open import Agda.Primitive

0ℓ : Level
0ℓ = lzero

testLevel : Level → Nat
testLevel _ = 

{-# FOREIGN AGDA2RUST
pub fn main () {
  println!("{}:\t\t {}", module_path!(),
    testLevel()
  );
}
#-}