Idris.DataOpts

Documentation

type ForceMap = IntMap Forceability

forceArgs :: Name -> Name -> [Int] -> Type -> Idris ()

getForcedArgs :: IState -> Name -> Type -> ForceMap

collapseCons :: Name -> [(Name, Type)] -> Idris ()

class Optimisable term where

Methods

applyOpts :: term -> Idris term

stripCollapsed :: term -> Idris term

Instances

Optimisable Raw

Optimisable a => Optimisable [a]

Optimisable (TT Name)

Optimisable (Binder (TT Name))

Optimisable (Binder Raw)

Optimisable a => Optimisable (Either a (a, a))

(Optimisable a, Optimisable b) => Optimisable (a, b)

(Optimisable a, Optimisable b) => Optimisable (vs, a, b)

forcedArgSeq :: OptInfo -> [Maybe Forceability]

forcedCnt :: ForceMap -> Int

applyDataOpt :: OptInfo -> Name -> [Raw] -> Raw

prel :: [Text]

applyDataOptRT :: OptInfo -> Name -> Int -> Int -> [Term] -> Term