Metavariables

module reflection.metavariables where

Imports

open import elementary-number-theory.natural-numbers

open import foundation.booleans
open import foundation.identity-types
open import foundation.universe-levels

open import primitives.strings

Idea

The Meta type represents metavariables in Agda.

Definition

postulate Meta : UU lzero
{-# BUILTIN AGDAMETA Meta #-}

primitive
  primMetaEquality : Meta → Meta → bool
  primMetaLess : Meta → Meta → bool
  primShowMeta : Meta → String
  primMetaToNat : Meta → ℕ
  primMetaToNatInjective : ∀ a b → primMetaToNat a ＝ primMetaToNat b → a ＝ b