Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Auto.Convert
Documentation
norm :: Normalise t => t -> TCM tSource
type O = (Maybe Int, QName)Source
data TMode Source
Constructors
TMAll
type MapS a b = (Map a b, [a])Source
data S Source
Constructors
S
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 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
getMeta :: MetaId -> TOM (Metavar (Exp O) (RefInfo O))Source
getEqs :: TCM [(Bool, Term, Term)]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
fmType :: MetaId -> Type -> BoolSource
fmExp :: MetaId -> Term -> BoolSource
frommyExp :: MExp O -> IO TermSource
frommyExps :: Nat -> MArgList O -> Term -> IO TermSource
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)) -> 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 :: Integer -> Integer -> Type -> Type -> Maybe (Nat, Nat)Source
Produced by Haddock version 2.6.1