Agda-2.6.2.1.20220320: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Rules.Builtin.Coinduction

Description

Handling of the INFINITY, SHARP and FLAT builtins.

Synopsis

Documentation

typeOfInf :: TCM Type Source #

The type of .

typeOfSharp :: TCM Type Source #

The type of ♯_.

typeOfFlat :: TCM Type Source #

The type of .

bindBuiltinInf :: ResolvedName -> TCM () Source #

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

bindBuiltinSharp :: ResolvedName -> TCM () Source #

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

bindBuiltinFlat :: ResolvedName -> TCM () Source #

Binds the FLAT builtin, and changes its definition.