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

Agda.Auto.Typecheck

Documentation

closify :: a -> Clos a o | Source

sub :: CExp o -> Clos a o -> Clos a o | Source

msubs :: [CExp o] -> a -> Clos a o | Source

weak :: Nat -> Clos a o -> Clos a o | Source

tcExp :: Bool -> Ctx o -> CExp o -> MExp o -> EE (MyPB o) | Source

tcargs :: Bool -> Ctx o -> CExp o -> CExp o -> MArgList o -> EE (MyPB o) | Source

hnn :: CExp o -> EE (MyMB (HNExp o) o) | Source

hnn' :: CExp o -> CArgList o -> EE (MyMB (HNExp o) o) | Source

hn' :: CExp o -> CArgList o -> EE (MyMB (HNExp o) o) | Source

data HNRes o | Source

Constructors

HNDone (HNExp o) |
HNMeta (CExp o) (CArgList o) |

hnc :: Bool -> CExp o -> CArgList o -> EE (MyMB (HNRes o) o) | Source

doclos :: [CAction o] -> Nat -> Either Nat (CExp o) | Source

hnarglist :: CArgList o -> EE (MyMB (HNArgList o) o) | Source

getNArgs :: Nat -> CArgList o -> EE (MyMB (Maybe ([CExp o], CArgList o)) o) | Source

getAllArgs :: CArgList o -> EE (MyMB [PEval o] o) | Source

iotastep :: HNExp o -> EE (MyMB (Maybe (CExp o, CArgList o)) o) | Source

data PEval o | Source

Constructors

PENo (CExp o) |
PEConApp (CExp o) (ConstRef o) [PEval o] |
PEConPar |

dorules :: [Clause o] -> [PEval o] -> EE (MyMB (Maybe (CExp o)) o) | Source

dorule :: Clause o -> [PEval o] -> EE (MyMB (Either (Maybe [PEval o]) (CExp o)) o) | Source

dopats :: [Pat o] -> [PEval o] -> EE (MyMB (Either (Maybe [PEval o]) ([PEval o], [CExp o])) o) | Source

dopat :: Pat o -> PEval o -> EE (MyMB (Either (Maybe (PEval o)) (PEval o, [CExp o])) o) | Source

noiotastep :: HNExp o -> EE (MyPB o) | Source

noiotastep' :: ConstRef o -> MArgList o -> EE (MyPB o) | Source

comp' :: CExp o -> CExp o -> EE (MyPB o) | Source

comp :: Bool -> CExp o -> CExp o -> EE (MyPB o) | Source

comphn' :: Bool -> HNExp o -> HNExp o -> EE (MyPB o) | Source

compargs :: CArgList o -> CArgList o -> EE (MyPB o) | Source

pickid :: MId -> MId -> MId | Source

tcSearch :: Ctx o -> CExp o -> MExp o -> EE (MyPB o) | Source

ptcTypeUnknown :: Bool -> Ctx o -> CExp o -> MExp o -> EE String | Source

ptcTypeCheck :: Bool -> Ctx o -> HNExp o -> MExp o -> EE String | Source

ptcTypecheckArgList :: String -> Bool -> Ctx o -> CExp o -> CExp o -> MArgList o -> EE String | Source

ptcNoIotaStep :: HNExp o -> EE String | Source

ptcCompare :: String -> Bool -> CExp o -> CExp o -> EE String | Source

ptcCompareArgList :: String -> CArgList o -> CArgList o -> EE String | Source

phnexp :: Bool -> Int -> [MId] -> HNExp o -> IO String | Source

phnargs :: Bool -> [MId] -> HNArgList o -> IO String | Source

pcexp :: Bool -> Int -> [MId] -> CExp o -> IO String | Source

pcargs :: Bool -> [MId] -> CArgList o -> IO String | Source

printCtx :: Bool -> Ctx o -> IO String | Source

Produced by Haddock version 2.4.2