Abstractions

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

open import primitives.strings

Idea

The Abs type represents a lambda abstraction.

Definition

data Abs {l} (A : UU l) : UU l where
  abs : String → A → Abs A

{-# BUILTIN ABS Abs #-}
{-# BUILTIN ABSABS abs #-}