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

Safe HaskellSafe-Infered

Agda.TypeChecking.Rules.Builtin.Coinduction

Description

Handling of the INFINITY, SHARP and FLAT builtins.

Synopsis

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.