Safe Haskell | None |
---|---|
Language | Haskell2010 |
- tcExp :: Bool -> Ctx o -> CExp o -> MExp o -> EE (MyPB o)
- getDatatype :: ICExp o -> EE (MyMB (Maybe (ICArgList o, [ConstRef o])) o)
- constructorImpossible :: ICArgList o -> ConstRef o -> EE (MyPB o)
- unequals :: ICArgList o -> ICArgList o -> ([(Nat, HNExp o)] -> EE (MyPB o)) -> [(Nat, HNExp o)] -> EE (MyPB o)
- unequal :: ICExp o -> ICExp o -> ([(Nat, HNExp o)] -> EE (MyPB o)) -> [(Nat, HNExp o)] -> EE (MyPB o)
- traversePi :: Int -> ICExp o -> EE (MyMB (HNExp o) o)
- tcargs :: Nat -> Bool -> Ctx o -> CExp o -> MArgList o -> MExp o -> Bool -> (CExp o -> MExp o -> EE (MyPB o)) -> EE (MyPB o)
- addend :: Hiding -> MExp o -> MM (Exp o) blk -> MM (Exp o) blk
- copyarg :: MExp o -> Bool
- type HNNBlks o = [HNExp o]
- noblks :: HNNBlks o
- addblk :: HNExp o -> HNNBlks o -> HNNBlks o
- hnn :: ICExp o -> EE (MyMB (HNExp o) o)
- hnn_blks :: ICExp o -> EE (MyMB (HNExp o, HNNBlks o) o)
- hnn_checkstep :: ICExp o -> EE (MyMB (HNExp o, Bool) o)
- hnn' :: ICExp o -> ICArgList o -> EE (MyMB (HNExp o, HNNBlks o) o)
- hnb :: ICExp o -> ICArgList o -> EE (MyMB (HNExp o) o)
- data HNRes o
- hnc :: Bool -> ICExp o -> ICArgList o -> [Maybe (UId o)] -> EE (MyMB (HNRes o) o)
- hnarglist :: ICArgList o -> EE (MyMB (HNArgList o) o)
- getNArgs :: Nat -> ICArgList o -> EE (MyMB (Maybe ([ICExp o], ICArgList o)) o)
- getAllArgs :: ICArgList o -> EE (MyMB [ICExp o] o)
- data PEval o
- iotastep :: Bool -> HNExp o -> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o)
- noiotastep :: HNExp o -> EE (MyPB o)
- noiotastep_term :: ConstRef o -> MArgList o -> EE (MyPB o)
- data CMode o
- data CMFlex o
- comp' :: forall o. Bool -> CExp o -> CExp o -> EE (MyPB o)
- checkeliminand :: MExp o -> EE (MyPB o)
- maybeor :: Bool -> Prio -> IO (PB (RefInfo o)) -> IO (PB (RefInfo o)) -> IO (PB (RefInfo o))
- iotapossmeta :: ICExp o -> ICArgList o -> EE Bool
- meta_not_constructor :: ICExp o -> EE (MB Bool (RefInfo o))
- calcEqRState :: EqReasoningConsts o -> MExp o -> EE (MyPB o)
- pickid :: MId -> MId -> MId
- tcSearch :: Bool -> Ctx o -> CExp o -> MExp o -> EE (MyPB o)
Documentation
tcExp :: Bool -> Ctx o -> CExp o -> MExp o -> EE (MyPB o) Source #
Typechecker drives the solution of metas.
unequals :: ICArgList o -> ICArgList o -> ([(Nat, HNExp o)] -> EE (MyPB o)) -> [(Nat, HNExp o)] -> EE (MyPB o) Source #
unequal :: ICExp o -> ICExp o -> ([(Nat, HNExp o)] -> EE (MyPB o)) -> [(Nat, HNExp o)] -> EE (MyPB o) Source #
tcargs :: Nat -> Bool -> Ctx o -> CExp o -> MArgList o -> MExp o -> Bool -> (CExp o -> MExp o -> EE (MyPB o)) -> EE (MyPB o) Source #
maybeor :: Bool -> Prio -> IO (PB (RefInfo o)) -> IO (PB (RefInfo o)) -> IO (PB (RefInfo o)) Source #
calcEqRState :: EqReasoningConsts o -> MExp o -> EE (MyPB o) Source #