Agda-2.2.10: A dependently typed functional programming language and proof assistant Source code Contents Index

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 Source

The type of &#x221e.

typeOfSharp :: TCM Type Source

The type of &#x266f_.

typeOfFlat :: TCM Type Source

The type of &#x266d.

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 nameOfInf :: QName nameOfSharp :: QName nameOfFlat :: QName

coinductionKit :: TCM (Maybe CoinductionKit) Source

Tries to build a CoinductionKit.

Produced by Haddock version 2.6.1