Agda.Auto.Convert

Documentation

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

type O = (Maybe Int, QName)

data TMode

Constructors

TMAll

Instances

Eq TMode

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

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

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

data S

Constructors

S

Fields

sConsts :: MapS QName (TMode, ConstRef O)

sMetas :: MapS MetaId (Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])

sEqs :: MapS Int (Maybe (Bool, MExp O, MExp O))

sCurMeta :: Maybe MetaId

sMainMeta :: MetaId

type TOM = StateT S TCM

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

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

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

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

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

copatternsNotImplemented :: TCM a

tomyClauses :: [Clause] -> StateT S (TCMT IO) [([Pat O], MExp O)]

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

tomyPat :: Arg Color Pattern -> StateT S (TCMT IO) (Pat O)

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

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

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

tomyType :: Type -> TOM (MExp O)

tomyExp :: Term -> TOM (MExp O)

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

tomyIneq :: Comparison -> Bool

fmType :: MetaId -> Type -> Bool

fmExp :: MetaId -> Term -> Bool

fmExps :: MetaId -> [Arg c Term] -> Bool

fmLevel :: MetaId -> PlusLevel -> Bool

cnvh :: LensHiding a => a -> FMode

icnvh :: FMode -> ArgInfo c

frommy :: MExp O -> ErrorT String IO Term

frommyType :: MExp O -> ErrorT String IO Type

frommyExp :: MExp O -> ErrorT String IO Term

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

abslamvarname :: [Char]

modifyAbstractExpr :: Expr -> Expr

modifyAbstractClause :: Clause -> Clause

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

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

contains_constructor :: [CSPat O] -> Bool

etaContractBody :: ClauseBody -> TCM ClauseBody

freeIn :: Nat -> MExp o -> Bool

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

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

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