Literals
Content created by Fredrik Bakke, Fernando Chu and Egbert Rijke.
Created on 2023-04-27.
Last modified on 2023-05-01.
module reflection.literals where
Imports
open import elementary-number-theory.natural-numbers open import foundation.universe-levels open import primitives.characters open import primitives.floats open import primitives.machine-integers open import primitives.strings open import reflection.metavariables open import reflection.names
Idea
The Literal
type represents literals in Agda.
For concrete examples, see
reflection.definitions
.
Definition
data Literal : UU lzero where nat : (n : ℕ) → Literal word64 : (n : Word64) → Literal float : (x : Float) → Literal char : (c : Char) → Literal string : (s : String) → Literal name : (x : Name) → Literal meta : (x : Meta) → Literal {-# BUILTIN AGDALITERAL Literal #-} {-# BUILTIN AGDALITNAT nat #-} {-# BUILTIN AGDALITWORD64 word64 #-} {-# BUILTIN AGDALITFLOAT float #-} {-# BUILTIN AGDALITCHAR char #-} {-# BUILTIN AGDALITSTRING string #-} {-# BUILTIN AGDALITQNAME name #-} {-# BUILTIN AGDALITMETA meta #-}
Recent changes
- 2023-05-01. Fredrik Bakke. Refactor 2, the sequel to refactor (#581).
- 2023-04-27. Egbert Rijke. fixing broken links (#580).
- 2023-04-27. Fernando Chu, Fernando Chu, Fernando Chu and Fredrik Bakke. Reflection and solvers (#571).