Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
Agda.Auto.CaseSplit
Documentation
abspatvarname :: String #
costCaseSplitLow :: Nat #
costAddVarDepth :: Nat #
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 #