idris-0.10: Functional Programming Language with Dependent Types
IRTS.Lang
data Endianness Source
Constructors
Instances
data LVar Source
data LExp Source
data FDesc Source
data Export Source
data ExportIFace Source
data PrimFn Source
data FCallType Source
data FType Source
data LAlt' e Source
type LAlt = LAlt' LExp Source
data LDecl Source
type LDefs = Ctxt LDecl Source
data LOpt Source
addTags :: Int -> [(Name, LDecl)] -> (Int, [(Name, LDecl)]) Source
data LiftState Source
lname :: Name -> Int -> Name Source
liftAll :: [(Name, LDecl)] -> [(Name, LDecl)] Source
lambdaLift :: Name -> LDecl -> [(Name, LDecl)] Source
getNextName :: State LiftState Name Source
addFn :: Name -> LDecl -> State LiftState () Source
lift :: [Name] -> LExp -> State LiftState LExp Source
allocUnique :: LDefs -> (Name, LDecl) -> (Name, LDecl) Source
usedArg :: (Eq t1, Foldable t) => t t1 -> t1 -> [t1] Source
usedIn :: [Name] -> LExp -> [Name] Source