Agda-2.2.10: A dependently typed functional programming language and proof assistant

Agda.Compiler.MAlonzo.Compiler

Synopsis

Documentation

definition :: Maybe CoinductionKit -> Definition -> TCM [Decl]

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

constructorArity :: MonadTCM tcm => QName -> tcm Nat

Move somewhere else!

argpatts :: [Arg Pattern] -> [Pat] -> TCM [Pat]

term :: Term -> ReaderT Nat TCM Exp

Extract Agda term to Haskell expression. Irrelevant arguments are extracted as (). Types are extracted as (). DontCare outside of irrelevant arguments is extracted as error.

term' :: Arg Term -> ReaderT Nat TCM Exp

Irrelevant arguments are replaced by Haskells' ().

tvaldecl

Arguments

:: QName 
-> Induction

Is the type inductive or coinductive?

-> Nat 
-> Nat 
-> [ConDecl] 
-> Maybe Clause 
-> [Decl] 

hsCast :: Exp -> Exp