Agda-2.2.10: A dependently typed functional programming language and proof assistant

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 :: Expr -> TCM ()
- bindBuiltinSharp :: Expr -> TCM ()
- bindBuiltinFlat :: Expr -> TCM ()
- data CoinductionKit = CoinductionKit {
  - nameOfInf :: QName
  - nameOfSharp :: QName
  - nameOfFlat :: QName
  }
- coinductionKit :: TCM (Maybe CoinductionKit)

# Documentation

typeOfInf :: TCM Type

The type of `&#x221e`.

typeOfSharp :: TCM Type

The type of `&#x266f_`.

typeOfFlat :: TCM Type

The type of `&#x266d`.

bindBuiltinInf :: Expr -> TCM ()

Binds the INFINITY builtin, but does not change the type's definition.

bindBuiltinSharp :: Expr -> TCM ()

Binds the SHARP builtin, and changes the definitions of INFINITY and SHARP.

bindBuiltinFlat :: Expr -> TCM ()

Binds the FLAT builtin, and changes its definition.

data CoinductionKit

The coinductive primitives.

Constructors

CoinductionKit |

Fields

nameOfInf :: QName
nameOfSharp :: QName
nameOfFlat :: QName

coinductionKit :: TCM (Maybe CoinductionKit)

Tries to build a `CoinductionKit`.