Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Inferred

Agda.Auto.CaseSplit

# Documentation

abspatvarname :: [Char]

costCaseSplitVeryHigh :: Int

costCaseSplitHigh :: Int

costCaseSplitLow :: Int

costAddVarDepth :: Int

data HI a

Constructors

HI FMode a |

drophid :: [HI b] -> [b]

type CSPat o = HI (CSPatI o)

type CSCtx o = [HI (MId, MExp o)]

data CSPatI o

Constructors

CSPatConApp (ConstRef o) [CSPat o] |
CSPatVar Nat |
CSPatExp (MExp o) |
CSWith (MExp o) |
CSAbsurd |
CSOmittedArg |

type Sol o = [(CSCtx o, [CSPat o], Maybe (MExp 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

replace :: Nat -> Nat -> MExp o -> MExp o -> MExp o

betareduce :: MExp o -> MArgList o -> MExp o

concatargs :: MM (ArgList o) (RefInfo o) -> MArgList o -> MArgList o

eqelr :: Elr o -> Elr o -> Bool

replacep :: Nat -> Nat -> CSPatI o -> MExp o -> CSPat o -> CSPat o

rm :: MM a b -> a

mm :: a -> MM a b

unifyexp :: MExp o -> MExp o -> Maybe [(Nat, MExp o)]

lift :: Nat -> MExp o -> MExp o

removevar :: CSCtx o -> MExp o -> [CSPat o] -> [(Nat, MExp o)] -> (CSCtx o, MExp o, [CSPat o])

notequal :: Nat -> Nat -> MExp o -> MExp o -> IO Bool

findperm :: [MExp o] -> Maybe [Nat]

freevars :: MExp o -> [Nat]

applyperm :: [Nat] -> CSCtx o -> MExp o -> [CSPat o] -> (CSCtx o, MExp o, [CSPat o])

ren :: Eq a => [a] -> a -> Int

rename :: (Nat -> Nat) -> MExp o -> MExp o

renamep :: (Nat -> Nat) -> CSPat o -> CSPat o

seqctx :: CSCtx o -> CSCtx o

depthofvar :: Nat -> [CSPat o] -> Nat

localTerminationEnv :: [CSPat o] -> ([Nat], Nat, [Nat])

localTerminationSidecond :: ([Nat], Nat, [Nat]) -> ConstRef o -> MExp o -> EE (MyPB o)

getblks :: MExp o -> IO [Nat]