Documentation

Converts a type from IR to Coq, lifting it into the Free monad.

\(\tau^\dagger = Free\,Shape\,Pos\,\tau^*\)

A type \(\tau\) is converted by lifting it into the Free monad and recursively converting the argument and return types of functions using convertType'.

Converts a type from IR to Coq.

In contrast to convertType, the type itself is not lifted into the Free monad. Only the argument and return types of the contained function type constructors are lifted recursively.

\(\alpha^* = \alpha'\)

A type variable \(\alpha\) is translated by looking up the corresponding Coq identifier \(\alpha'\).

\(T^* = T'\,Shape\,Pos\)

A type constructor \(T\) is translated by looking up the corresponding Coq identifier \(T'\) and adding the parameters \(Shape\) and \(Pos\).

\((\tau_1\,\tau_2)^* = \tau_1^*\,\tau_2^*\)

Type constructor applications are translated recursively but remain unchanged otherwise.

\((\tau_1 \rightarrow \tau_2)^* = \tau_1^\dagger \rightarrow \tau_2^\dagger\)

Type constructor applications are translated recursively but remain unchanged otherwise.

Converts a given type in the lifted IR to a Coq term.