Abstractions
Content created by Fredrik Bakke and Fernando Chu.
Created on 2023-04-27.
Last modified on 2023-05-01.
module reflection.abstractions where
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
- 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).