Agda-2.6.2.1: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Compiler.Treeless.NormalizeNames

Description

Ensures that all occurences of an abstract name share the same concrete name.

Apply this transformation if your backend uses concrete names for identification purposes!

The identity of an abstract name is only the nameId, the concrete name is only a naming suggestion. If renaming imports are used, the concrete name may change. This transformation makes sure that all occurences of an abstract name share the same concrete name.

This transfomation should be run as the last transformation.

Documentation