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.

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

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

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).