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

Agda.TypeChecking.Rules.Builtin.Coinduction

Description

Handling of the INFINITY, SHARP and FLAT builtins.

Synopsis

Documentation

The type of ∞.

The type of ♯_.

The type of ♭.

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

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

Binds the FLAT builtin, and changes its definition.