Agda-2.5.2: A dependently typed functional programming language and proof assistant

Safe HaskellSafe
LanguageHaskell2010

Agda.Auto.SearchControl

Contents

Documentation

extraref :: UId o -> [Maybe (UId o)] -> ConstRef o -> (Int, StateT (IORef [SubConstraints (RefInfo o)], Int) IO (Exp o)) Source #

Orphan instances

Trav a blk => Trav [a] blk Source # 

Methods

trav :: Monad m => (forall b. Trav b blk => MM b blk -> m ()) -> [a] -> m () Source #

Refinable (ICExp o) (RefInfo o) Source # 

Methods

refinements :: RefInfo o -> [RefInfo o] -> Metavar (ICExp o) (RefInfo o) -> IO [(Int, RefCreateEnv (RefInfo o) (ICExp o))] Source #

Refinable (ArgList o) (RefInfo o) Source # 

Methods

refinements :: RefInfo o -> [RefInfo o] -> Metavar (ArgList o) (RefInfo o) -> IO [(Int, RefCreateEnv (RefInfo o) (ArgList o))] Source #

Refinable (Exp o) (RefInfo o) Source # 

Methods

refinements :: RefInfo o -> [RefInfo o] -> Metavar (Exp o) (RefInfo o) -> IO [(Int, RefCreateEnv (RefInfo o) (Exp o))] Source #

Refinable (ConstRef o) (RefInfo o) Source # 

Methods

refinements :: RefInfo o -> [RefInfo o] -> Metavar (ConstRef o) (RefInfo o) -> IO [(Int, RefCreateEnv (RefInfo o) (ConstRef o))] Source #

Trav (ArgList o) (RefInfo o) Source # 

Methods

trav :: Monad m => (forall b. Trav b (RefInfo o) => MM b (RefInfo o) -> m ()) -> ArgList o -> m () Source #

Trav (Exp o) (RefInfo o) Source # 

Methods

trav :: Monad m => (forall b. Trav b (RefInfo o) => MM b (RefInfo o) -> m ()) -> Exp o -> m () Source #

Trav (MId, CExp o) (RefInfo o) Source # 

Methods

trav :: Monad m => (forall b. Trav b (RefInfo o) => MM b (RefInfo o) -> m ()) -> (MId, CExp o) -> m () Source #

Trav (TrBr a o) (RefInfo o) Source # 

Methods

trav :: Monad m => (forall b. Trav b (RefInfo o) => MM b (RefInfo o) -> m ()) -> TrBr a o -> m () Source #