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

Safe Haskell | Safe-Infered

Agda.TypeChecking.CompiledClause.Compile

# Documentation

compileClauses

Arguments

:: Bool | Translate record patterns?
-> [Clause] |
-> TCM CompiledClauses |

type Cl = ([Arg Pattern], ClauseBody)

type Cls = [Cl]

compile :: Cls -> CompiledClauses

nextSplit :: Cls -> Maybe Int

splitOn :: Int -> Cls -> Case Cls

splitC :: Int -> Cl -> Case Cl

expandCatchAlls :: Int -> Cls -> Cls

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