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

Agda.Compiler.MAlonzo.Compiler

Synopsis

Documentation

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

Move somewhere else!

tvaldeclSource

Arguments

:: QName 
-> Induction

Is the type inductive or coinductive?

-> Nat 
-> Nat 
-> [HsConDecl] 
-> Maybe Clause 
-> [HsDecl]