Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.TypeChecking.Rules.Builtin.Coinduction
Description
Handling of the INFINITY, SHARP and FLAT builtins.
Synopsis
typeOfInf :: TCM Type
typeOfSharp :: TCM Type
typeOfFlat :: TCM Type
bindBuiltinInf :: Expr -> TCM ()
bindBuiltinSharp :: Expr -> TCM ()
bindBuiltinFlat :: Expr -> TCM ()
data CoinductionKit = CoinductionKit {
nameOfInf :: QName
nameOfSharp :: QName
nameOfFlat :: QName
}
coinductionKit :: TCM (Maybe CoinductionKit)
Documentation
typeOfInf :: TCM TypeSource
The type of &#x221e.
typeOfSharp :: TCM TypeSource
The type of &#x266f_.
typeOfFlat :: TCM TypeSource
The type of &#x266d.
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.
data CoinductionKit Source
The coinductive primitives.
Constructors
CoinductionKit
nameOfInf :: QName
nameOfSharp :: QName
nameOfFlat :: QName
coinductionKit :: TCM (Maybe CoinductionKit)Source
Tries to build a CoinductionKit.
Produced by Haddock version 2.6.1