Documentation

Converts the declarations of type variables in the head of a data type or type synonym declaration to a Coq binder for a set of explicit or implicit type arguments.

E.g. the declaration of the type variable a in data D a = ... is translated to the binder (a : Type). If there are multiple type variable declarations as in data D a b = ... they are grouped into a single binder (a b : Type), because we assume all Haskell type variables to be of kind *.

The first argument controls whether the generated binders are explicit (e.g. (a : Type)) or implicit (e.g. {a : Type}).

Like convertTypeVarDecls but also returns the Coq identifiers of the bound variables.

Converts the argument of a function (a variable pattern) to an explicit Coq binder.

If the variable pattern has a type annotation, the generated binder is annotated with the converted type. If the variable pattern is strict, the variable is marked as non-monadic and the converted type is not lifted to the Free monad.

Generates an explicit Coq binder for a function argument with the given name and optional Coq type.

If no type is provided, it will be inferred by Coq.

Converts the argument of an artificially generated function to an explicit Coq binder. A fresh Coq identifier is selected for the argument and returned together with the binder.