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

Agda.TypeChecking.CompiledClause.Compile

Documentation

compileClausesSource

Arguments

:: Bool

Translate record patterns?

-> [Clause] 
-> TCM CompiledClauses 

type Cl = ([Arg Pattern], ClauseBody)Source

type Cls = [Cl]Source

compile :: Cls -> CompiledClausesSource

nextSplit :: Cls -> Maybe IntSource

splitOn :: Int -> Cls -> Case ClsSource

splitC :: Int -> Cl -> Case ClSource

expandCatchAlls :: Int -> Cls -> ClsSource

substBody :: Int -> Integer -> Term -> ClauseBody -> ClauseBodySource