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
- 2023-05-01. Fredrik Bakke. Refactor 2, the sequel to refactor (#581).
- 2023-04-27. Fernando Chu, Fernando Chu, Fernando Chu and Fredrik Bakke. Reflection and solvers (#571).