Module minitt::read_back

Read back: read back functions.

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

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 and normal.

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.