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

Abstractions

module reflection.abstractions where
Imports 
open import foundation.universe-levels

open import primitives.strings

Idea

The Abstraction-Agda type represents a lambda abstraction.

Definition

data Abstraction-Agda {l : Level} (A : UU l) : UU l where
  cons-Abstraction-Agda : String → A → Abstraction-Agda A

{-# BUILTIN ABS Abstraction-Agda #-}
{-# BUILTIN ABSABS cons-Abstraction-Agda #-}