Safe Haskell | Safe-Infered |
---|
Agda.Auto.CaseSplit
Documentation
abspatvarname :: [Char]
data CSPatI o
caseSplitSearch :: forall o. IORef Int -> Int -> [ConstRef o] -> Maybe (EqReasoningConsts o) -> Int -> Int -> ConstRef o -> CSCtx o -> MExp o -> [CSPat o] -> IO [Sol o]
caseSplitSearch' :: forall o. (Int -> CSCtx o -> MExp o -> ([Nat], Nat, [Nat]) -> IO (Maybe (MExp o))) -> Int -> Int -> ConstRef o -> CSCtx o -> MExp o -> [CSPat o] -> IO [Sol o]
infertypevar :: CSCtx o -> Nat -> MExp o
betareduce :: MExp o -> MArgList o -> MExp o
depthofvar :: Nat -> [CSPat o] -> Nat
localTerminationEnv :: [CSPat o] -> ([Nat], Nat, [Nat])