Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




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

Note that the INFINITY, SHARP and FLAT builtins are translated as follows (if a CoinductionKit is given):

   type Infinity a b = b

sharp :: a -> a
   sharp x = x

flat :: a -> a
   flat x = x

conArityAndPars :: QName -> TCM (Nat, Nat)Source

Move somewhere else!

term :: Term -> ReaderT Nat TCM ExpSource

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 ExpSource

Irrelevant arguments are replaced by Haskells' ().



:: QName 
-> Induction

Is the type inductive or coinductive?

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