The type of ∞.
ModuleAgda-2.7.0.1Haskell2010
Agda.TypeChecking.Rules.Builtin.Coinduction
Handling of the INFINITY, SHARP and FLAT builtins.
- 6 values
- PackageAgda-2.7.0.1
- 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.