Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Auto.CaseSplit
Documentation
data HI a Source
Constructors
HI FMode a
type CSPat o = HI (CSPatI o)Source
type CSCtx o = [HI (MId, MExp o)]Source
data CSPatI o Source
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))]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
infertypevar :: CSCtx o -> Nat -> MExp oSource
replace :: Nat -> Nat -> MExp o -> MExp o -> MExp oSource
betareduce :: MExp o -> MArgList 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
findperm :: [MExp o] -> Maybe [Nat]Source
freevars :: MExp o -> [Nat]Source
applyperm :: [Nat] -> CSCtx o -> MExp o -> [CSPat o] -> (CSCtx o, MExp o, [CSPat o])Source
rename :: (Nat -> Nat) -> MExp o -> MExp oSource
renamep :: (Nat -> Nat) -> CSPat o -> CSPat oSource
seqctx :: CSCtx o -> CSCtx oSource
depthofvar :: Nat -> [CSPat o] -> NatSource
localTerminationEnv :: [CSPat o] -> ([Nat], Nat, [Nat])Source
localTerminationSidecond :: ([Nat], Nat, [Nat]) -> ConstRef o -> MExp o -> EE (MyPB o)Source
getblks :: MExp o -> IO [Nat]Source
Produced by Haddock version 2.6.1