The names and types of the parameters that must be passed to the Free monad. These parameters are added automatically to every defined type and function.

shapeIdent :: Ident Source #

Like shape but not wrapped in a Bare constructor.

posIdent :: Ident Source #

Like pos but not wrapped in a Bare constructor.

forFree :: Qualid Source #

The Coq identifier for the ForFree property.

Partiality

partial :: Qualid Source #

The Coq identifier for the Partial type class.

partialArg :: Qualid Source #

The Coq identifier for the argument of the Partial type class.

partialUndefined :: Qualid Source #

The identifier for the error term undefined.

partialError :: Qualid Source #

The identifier for the error term error.

Tracing

traceable :: Qualid Source #

The Coq identifier for the Traceable type class.

traceableArg :: Qualid Source #

The Coq identifier for the argument of the Traceable type class.

trace :: Qualid Source #

The identifier for the effect trace.

Non-Determinism

nonDet :: Qualid Source #

The Coq identifier for the NonDet type class.

nonDetArg :: Qualid Source #

The Coq identifier for the argument of the NonDet type class.

Modules

qualifiedSmartConstructorModule :: Ident Source #

The name of the local module, where qualified smart constructor notations are defined.

Sharing

strategy :: Qualid Source #

The Coq identifier for the Strategy type class.

strategyArg :: Qualid Source #

The Coq identifier for the argument of the Strategy type class.

strategyBinder :: Binder Source #

shareableArgs :: Qualid Source #

The Coq identifier for the ShareableArgs type class.

shareableArgsBinder :: Qualid -> Binder Source #

The Coq binder for the ShareableArgs type class with the type variable with the given name.

shareArgs :: Qualid Source #

The Coq identifier of the ShareableArgs class function.

normalform :: Qualid Source #

The Coq identifier for the Normalform type class.

normalformBinder :: Qualid -> Binder Source #

The Coq binder for the Normalform type class with the source and target type variable with the given names.

nf' :: Qualid Source #

The Coq identifier of the Normalform class function.

nf :: Qualid Source #

The Coq identifier of the function nf.

nType :: Qualid Source #

The Coq identifier for a normalized type.

implicitArg :: Term Source #

The Coq identifier for an implicit argument.

share :: Qualid Source #

The Coq identifier for the share operator.

shareWith :: Qualid Source #

The Coq identifier for the shareWith operator.

Effect Selection

selectExplicitArgs :: Effect -> [Term] Source #

Selects the correct explicit function arguments for the given effect.

selectImplicitArgs :: Effect -> [Term] Source #

Selects the correct implicit function arguments for the given effect.

selectTypedImplicitArgs :: Effect -> Int -> [Term] Source #

Like selectImplicitArgs but the arguments have to be inserted after the type arguments the specified number of times.

selectBinders :: Effect -> [Binder] Source #

Selects the correct binder for the given effect.

selectTypedBinders :: Effect -> [Qualid] -> [Binder] Source #

Like selectBinders but the binders are dependent on the type variables with the given names.

Literal Scopes

integerScope :: Ident Source #

The scope of integer literals.

stringScope :: Ident Source #

The scope of string literals used in error terms.

Tactics

proveInd :: Qualid Source #

The tactic that is needed to prove induction schemes.

Reserved Identifiers

reservedIdents :: [Qualid] Source #

All Coq identifiers that are reserved for the Base library.

This does only include identifiers without corresponding Haskell name.