Metavariables

Content created by Fredrik Bakke and Fernando Chu.

Created on 2023-04-27.
Last modified on 2023-05-01.

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

Recent changes