|
Agda.Compiler.MAlonzo.Compiler |
|
|
|
Synopsis |
|
|
|
Documentation |
|
|
|
|
|
|
|
|
|
|
Note that the INFINITY, SHARP and FLAT builtins are translated as
follows (if a CoinductionKit is given):
type Infinity a b = b
sharp :: forall a. () -> forall b. () -> b -> b
sharp _ _ x = x
flat :: forall a. () -> forall b. () -> b -> b
flat _ _ x = x
|
|
|
|
|
|
|
Move somewhere else!
|
|
|
|
|
|
|
|
|
Extract Agda term to Haskell expression.
Irrelevant arguments are extracted as ().
Types are extracted as ().
DontCare outside of irrelevant arguments is extracted as error.
|
|
|
Irrelevant arguments are replaced by Haskells' ().
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Produced by Haddock version 2.6.1 |