The type of ∞.
ModuleAgda-2.8.0.2Haskell2010
Agda.TypeChecking.Rules.Builtin.Coinduction
Handling of the INFINITY, SHARP and FLAT builtins.
Synopsis
- value typeOfInf
- value typeOfSharp
- value typeOfFlat
- value bindBuiltinInf
- value bindBuiltinSharp
- value bindBuiltinFlat
- PackageAgda-2.8.0.2
- Exports6
- LanguageHaskell2010
- LicenceMIT
- SourceCoinduction.hs
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.