Agda-2.2.6: A dependently typed functional programming language and proof assistant
Agda.Auto.Convert
norm :: Normalise t => t -> TCM tSource
type O = (Maybe Int, QName)Source
data TMode Source
Constructors
Instances
type MapS a b = (Map a b, [a])Source
data S Source
Fields
type TOM = StateT S TCMSource
tomy :: MetaId -> [(Bool, QName)] -> TCM ([ConstRef 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 -> IO ArgsSource