Agda.TypeChecking.Rules.Builtin.Coinduction
Description
Handling of the INFINITY, SHARP and FLAT builtins.
- typeOfInf :: TCM Type
- typeOfSharp :: TCM Type
- typeOfFlat :: TCM Type
- bindBuiltinInf :: Expr -> TCM ()
- bindBuiltinSharp :: Expr -> TCM ()
- bindBuiltinFlat :: Expr -> TCM ()
- data CoinductionKit = CoinductionKit {
- nameOfInf :: QName
- nameOfSharp :: QName
- nameOfFlat :: QName
- coinductionKit :: TCM (Maybe CoinductionKit)
Documentation
The type of ♯_.
The type of ♭.
bindBuiltinInf :: Expr -> TCM ()Source
Binds the INFINITY builtin, but does not change the type's definition.
bindBuiltinSharp :: Expr -> TCM ()Source
Binds the SHARP builtin, and changes the definitions of INFINITY and SHARP.
bindBuiltinFlat :: Expr -> TCM ()Source
Binds the FLAT builtin, and changes its definition.
data CoinductionKit Source
The coinductive primitives.
Constructors
| CoinductionKit | |
Fields
| |
coinductionKit :: TCM (Maybe CoinductionKit)Source
Tries to build a CoinductionKit.