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

Safe HaskellSafe-Inferred

Agda.Auto.CaseSplit

Documentation

data HI a Source

Constructors

HI FMode a 

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

type CSPat o = HI (CSPatI o)Source

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

type Sol o = [(CSCtx o, [CSPat o], Maybe (MExp o))]Source

caseSplitSearch :: forall o. IORef Int -> Int -> [ConstRef o] -> Maybe (EqReasoningConsts o) -> Int -> Int -> ConstRef o -> CSCtx o -> MExp o -> [CSPat o] -> IO [Sol o]Source

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]Source

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

eqelr :: Elr o -> Elr o -> BoolSource

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

rm :: MM a b -> aSource

mm :: a -> MM a bSource

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

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

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

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

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

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

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

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