This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

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 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 #-}