Abstractions

Content created by Fredrik Bakke and Fernando Chu.

Created on 2023-04-27.
Last modified on 2023-05-01.

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

Recent changes