idris-0.9.17: Functional Programming Language with Dependent Types

Safe HaskellNone
LanguageHaskell98

IRTS.Simplified

Documentation

simplifyDefs :: DDefs -> [(Name, DDecl)] -> TC [(Name, SDecl)] Source

data SDecl Source

Constructors

SFun Name [Name] Int SExp 

Instances

data SExp Source

Constructors

SV LVar 
SApp Bool Name [LVar] 
SLet LVar SExp SExp 
SUpdate LVar SExp 
SCon (Maybe LVar) Int Name [LVar] 
SCase CaseType LVar [SAlt] 
SChkCase LVar [SAlt] 
SProj LVar Int 
SConst Const 
SForeign FDesc FDesc [(FDesc, LVar)] 
SOp PrimFn [LVar] 
SNothing 
SError String 

Instances

data SAlt Source

Constructors

SConCase Int Int Name [Name] SExp 
SConstCase Const SExp 
SDefaultCase SExp 

Instances