| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Rules.Builtin.Coinduction
Description
Handling of the INFINITY, SHARP and FLAT builtins.
Synopsis
- typeOfInf :: TCM Type
- typeOfSharp :: TCM Type
- typeOfFlat :: TCM Type
- bindBuiltinInf :: ResolvedName -> TCM ()
- bindBuiltinSharp :: ResolvedName -> TCM ()
- bindBuiltinFlat :: ResolvedName -> TCM ()
Documentation
typeOfSharp :: TCM Type Source #
The type of ♯_.
typeOfFlat :: TCM Type Source #
The type of ♭.
bindBuiltinInf :: ResolvedName -> TCM () Source #
Binds the INFINITY builtin, but does not change the type's definition.
bindBuiltinSharp :: ResolvedName -> TCM () Source #
Binds the SHARP builtin, and changes the definitions of INFINITY and SHARP.
bindBuiltinFlat :: ResolvedName -> TCM () Source #
Binds the FLAT builtin, and changes its definition.