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

Safe HaskellNone
LanguageHaskell98

Agda.Compiler.MAlonzo.Misc

Contents

Synopsis

Documentation

Types coming from Agda are named T\<number\>.

Other definitions coming from Agda are named "d<number>".

Names coming from Haskell must always be used qualified.

duname :: QName -> Name Source

Name for definition stripped of unused arguments

hspLet :: Pat -> Exp -> Exp -> Exp Source

hsLet :: Name -> Exp -> Exp -> Exp Source

hsMapAlt :: (Exp -> Exp) -> Alt -> Alt Source

hsMapRHS :: (Exp -> Exp) -> Rhs -> Rhs Source