Module minitt::check::read_back

Read back: read back functions and normal form definitions.

Converting terms to normal forms with de-bruijn indices so we do not need to deal with alpha conversions when checking syntactic-equality.

Functions in this module are put into impl for blocks, their docs can be found in:

• ReadBack of Value
• ReadBack of Telescope
• ReadBack of Closure

Depends on modules syntax.

Enums

NormalExpression

NExp in Mini-TT, normal form expressions. Deriving Eq so we can do comparison.

Traits

ReadBack

Since all of Value, Neutral and Telescope have a read back function, I extracted this common interface for them.

Functions

generate_value	genV in Mini-TT.
read_back_branches

Type Definitions

NormalCase
NormalCaseTree	NSClos in Mini-TT, normal form closures.
NormalNeutral	NNeut in Mini-TT, normal form neutral values.
NormalTelescope	NRho in Mini-TT, normal form telescopes (contexts).