Bind a builtin thing to an expression.
ModuleAgda-2.8.0.2Haskell2010
Agda.TypeChecking.Rules.Builtin
Synopsis
- value bindBuiltin
- value bindBuiltinNoDef
- value builtinKindOfName
- value bindPostulatedName
- value isUntypedBuiltin
- value bindUntypedBuiltin
- PackageAgda-2.8.0.2
- Exports6
- LanguageHaskell2010
- LicenceMIT
- SourceBuiltin.hs
Bind a builtin thing to a new name.
Since their type is closed, it does not matter whether we are in a parameterized module when we declare them. We simply ignore the parameters.
bindPostulatedName builtin q m checks that q is a postulated
name, and binds the builtin builtin to the term m q def,
where def is the current Definition of q.