Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone



Handling of the INFINITY, SHARP and FLAT builtins.



typeOfInf :: TCM TypeSource

The type of .

typeOfSharp :: TCM TypeSource

The type of ♯_.

typeOfFlat :: TCM TypeSource

The type of .

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.