Agda-2.2.10: A dependently typed functional programming language and proof assistant Source code Contents Index

Agda.Auto.Convert

Documentation

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

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

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

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

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

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

fmType :: MetaId -> Type -> Bool Source

fmExp :: MetaId -> Term -> Bool Source

frommyExp :: MExp O -> IO Term Source

frommyExps :: Nat -> MArgList O -> Term -> IO Term Source

modifyAbstractExpr :: Expr -> Expr Source

modifyAbstractClause :: Clause -> Clause Source

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

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

contains_constructor :: [CSPat O] -> Bool Source

etaContractBody :: ClauseBody -> TCM ClauseBody Source

freeIn :: Nat -> MExp o -> Bool Source

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

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

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

Produced by Haddock version 2.6.1