Idris.DataOpts

Documentation

class Optimisable term where

Methods

applyOpts :: 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)

prel :: [Text]

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