Safe Haskell | None |
---|---|
Language | Haskell98 |
Agda.Auto.Convert
Documentation
popMapS :: MonadState s m => (s -> (t, [a])) -> ((t, [a]) -> s -> s) -> m (Maybe a)
data S
tomy :: MetaId -> [(Bool, QName)] -> [Type] -> TCM ([ConstRef O], [MExp O], Map MetaId (Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [MetaId]), [(Bool, MExp O, MExp O)], Map QName (TMode, ConstRef O))
tomyIneq :: Comparison -> Bool
cnvh :: LensHiding a => a -> FMode
abslamvarname :: [Char]
modifyAbstractExpr :: Expr -> Expr
modifyAbstractClause :: Clause -> Clause
constructPats :: Map QName (TMode, ConstRef O) -> MetaId -> Clause -> TCM ([(FMode, MId)], [CSPat O])
contains_constructor :: [CSPat O] -> Bool