idris

Safe Haskell	None

Idris.DataOpts

Documentation

forceArgs :: Name -> Type -> Idris ()Source

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

class Optimisable term whereSource

Methods

applyOpts :: term -> Idris termSource

stripCollapsed :: term -> Idris termSource

Instances

Optimisable Raw
Optimisable a => Optimisable [a]
Optimisable (TT Name)
Optimisable t => Optimisable (Binder t)
Optimisable a => Optimisable (Either a (a, a))
(Optimisable a, Optimisable b) => Optimisable (a, b)
(Optimisable a, Optimisable b) => Optimisable (vs, a, b)

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

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