Abstractions

Content created by Fredrik Bakke and Fernando Chu.

Created on 2023-04-27.
Last modified on 2024-02-07.

module reflection.abstractions where

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

Recent changes

• 2024-02-07. Fredrik Bakke. Deduplicate definitions (#1022).
• 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).