Metavariables

Content created by Fredrik Bakke, Fernando Chu and Egbert Rijke.

Created on 2023-04-27.
Last modified on 2026-05-02.

module reflection.metavariables where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.universe-levels

open import foundation-core.booleans
open import foundation-core.identity-types

open import lists.lists

open import primitives.strings

Idea

The Metavariable-Agda type represents metavariables in Agda.

Definition

postulate
  Metavariable-Agda : UU lzero

{-# BUILTIN AGDAMETA Metavariable-Agda #-}

primitive
  primMetaEquality :
    Metavariable-Agda → Metavariable-Agda → bool
  primMetaLess :
    Metavariable-Agda → Metavariable-Agda → bool
  primShowMeta :
    Metavariable-Agda → String
  primMetaToNat :
    Metavariable-Agda → ℕ
  primMetaToNatInjective :
    (a b : Metavariable-Agda) → primMetaToNat a ＝ primMetaToNat b → a ＝ b

data Blocker-Agda : UU lzero where
  any-Blocker-Agda : list Blocker-Agda → Blocker-Agda
  all-Blocker-Agda : list Blocker-Agda → Blocker-Agda
  metavariable-Blocker-Agda : Metavariable-Agda → Blocker-Agda

{-# BUILTIN AGDABLOCKER Blocker-Agda #-}
{-# BUILTIN AGDABLOCKERANY any-Blocker-Agda #-}
{-# BUILTIN AGDABLOCKERALL all-Blocker-Agda #-}
{-# BUILTIN AGDABLOCKERMETA metavariable-Blocker-Agda #-}

Recent changes