Reflection
Content created by Egbert Rijke, Fredrik Bakke and Fernando Chu.
Created on 2023-04-27.
Last modified on 2024-04-19.
{-# OPTIONS --rewriting #-}
Files in the reflection folder
module reflection where open import reflection.abstractions public open import reflection.arguments public open import reflection.boolean-reflection public open import reflection.definitions public open import reflection.erasing-equality public open import reflection.fixity public open import reflection.group-solver public open import reflection.literals public open import reflection.metavariables public open import reflection.names public open import reflection.precategory-solver public open import reflection.rewriting public open import reflection.terms public open import reflection.type-checking-monad public
Recent changes
- 2024-04-19. Fredrik Bakke. Rewrite rules for pushouts (#1021).
- 2023-05-06. Egbert Rijke. Collecting some easily defined precategories (#598).
- 2023-05-06. Egbert Rijke. Big cleanup throughout library (#594).
- 2023-04-27. Fernando Chu, Fernando Chu, Fernando Chu and Fredrik Bakke. Reflection and solvers (#571).