| Agda-2.2.6: 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 |

Instances

Eq TMode

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 |

type TOM = StateT S TCM | Source

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 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 -> IO Args | Source

Produced by Haddock version 2.4.2