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

class Replace o t u

replace

betareduce

concatargs

replacep

type Assignments o

class Unify o t

unify

notequal

unifyVar

unifyexp

class Lift t

lift

removevar

findperm

freevars

applyperm

ren

seqctx

depthofvar

class LocalTerminationEnv a

localTerminationEnv

localTerminationSidecond

getblks