Rewriting

Content created by Fredrik Bakke.

Created on 2024-04-19.
Last modified on 2024-04-19.

{-# OPTIONS --rewriting #-}

module reflection.rewriting where
Imports 
open import foundation-core.identity-types

Idea

Agda’s rewriting functionality allows us to add new strict equalities to our type theory. Given an identification β : x ＝ y, then adding a rewrite rule for β with

{-# REWRITE β #-}

will make it so x rewrites to y, i.e., x ≐ y.

Warning. Rewriting is by nature a very unsafe tool so we advice exercising abundant caution when defining such rules.

Definitions

We declare to Agda that the standard identity relation may be used to define rewrite rules.

{-# BUILTIN REWRITE _＝_ #-}

See also

Recent changes