Agda.Auto.CaseSplit

abspatvarname

costCaseSplitVeryHigh

costCaseSplitHigh

costCaseSplitLow

costAddVarDepth

data HI a

drophid

type CSPat o

type CSCtx o

data CSPatI o

type Sol o

caseSplitSearch

caseSplitSearch'

infertypevar

replace

betareduce

concatargs

eqelr

replacep

rm

mm

unifyexp

lift

removevar

notequal

findperm

freevars

applyperm

ren

rename

renamep

seqctx

depthofvar

localTerminationEnv

localTerminationSidecond

getblks