Documentation

norm :: Normalise t => t -> TCM tSource

type O = (Maybe Int, QName)Source

data TMode Source

type MapS a b = (Map a b, [a])Source

initMapS :: (Map k a, [a1])Source

popMapS :: MonadState s m => (s -> (t, [a])) -> ((t, [a]) -> s -> s) -> m (Maybe a)Source

data S Source

type TOM = StateT S TCMSource

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))Source

getConst :: Bool -> QName -> TMode -> TOM (ConstRef O)Source

getdfv :: MetaId -> QName -> TCMT IO NatSource

getMeta :: MetaId -> TOM (Metavar (Exp O) (RefInfo O))Source

getEqs :: TCM [(Bool, Term, Term)]Source

tomyClauses :: [Clause] -> StateT S TCM [([Pat O], MExp O)]Source

tomyClause :: Clause -> StateT S TCM (Maybe ([Pat O], MExp O))Source

tomyPat :: Arg Pattern -> StateT S TCM (Pat O)Source

tomyBody :: Num t => ClauseBody -> StateT S (TCMT IO) (Maybe (MExp O, t))Source

weaken :: Int -> MExp O -> MExp OSource

weakens :: Int -> MArgList O -> MArgList OSource

tomyType :: Type -> TOM (MExp O)Source

tomyExp :: Term -> TOM (MExp O)Source

tomyExps :: [Arg Term] -> StateT S TCM (MM (ArgList O) (RefInfo O))Source

tomyIneq :: Comparison -> BoolSource

fmType :: MetaId -> Type -> BoolSource

fmExp :: MetaId -> Term -> BoolSource

fmExps :: MetaId -> [Arg Term] -> BoolSource

fmLevel :: MetaId -> PlusLevel -> BoolSource

cnvh :: Hiding -> FModeSource

icnvh :: FMode -> HidingSource

frommy :: MExp O -> ErrorT String IO TermSource

frommyType :: MExp O -> ErrorT String IO TypeSource

frommyExp :: MExp O -> ErrorT String IO TermSource

frommyExps :: Nat -> MArgList O -> Term -> ErrorT String IO TermSource

abslamvarname :: [Char]Source

modifyAbstractExpr :: Expr -> ExprSource

modifyAbstractClause :: Clause -> ClauseSource

constructPats :: Map QName (TMode, ConstRef O) -> MetaId -> Clause -> TCM ([(FMode, MId)], [CSPat O])Source

frommyClause :: (CSCtx O, [CSPat O], Maybe (MExp O)) -> ErrorT String IO ClauseSource

contains_constructor :: [CSPat O] -> BoolSource

etaContractBody :: ClauseBody -> TCM ClauseBodySource

freeIn :: Nat -> MExp o -> BoolSource

negtype :: ConstRef o -> MExp o -> MExp oSource

findClauseDeep :: MetaId -> TCM (Maybe (QName, Clause, Bool))Source

matchType :: Int -> Int -> Type -> Type -> Maybe (Nat, Nat)Source