Safe Haskell | Safe-Inferred |
---|
Agda.Auto.Typecheck
Documentation
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)
tcargs :: Nat -> Bool -> Ctx o -> CExp o -> MArgList o -> MExp o -> Bool -> (CExp o -> MExp o -> EE (MyPB o)) -> EE (MyPB o)
noblks :: [a]
addblk :: a -> [a] -> [a]
data HNRes o
getAllArgs :: ICArgList o -> EE (MyMB [ICExp o] o)
noiotastep :: HNExp o -> EE (MyPB o)
noiotastep_term :: ConstRef o -> MArgList o -> EE (MyPB o)
data CMode o
data CMFlex o
checkeliminand :: MExp o -> EE (MyPB o)
maybeor :: t -> t1 -> t3 -> t2 -> t3
iotapossmeta :: ICExp o -> ICArgList o -> EE Bool
calcEqRState :: EqReasoningConsts o -> MExp o -> EE (MyPB o)