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

Safe Haskell	Safe-Infered

Agda.TypeChecking.CompiledClause.Compile

Documentation

compileClauses Source

Arguments

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

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

type Cls = [Cl]Source

compile :: Cls -> CompiledClauses Source

nextSplit :: Cls -> Maybe Int Source

splitOn :: Int -> Cls -> Case Cls Source

splitC :: Int -> Cl -> Case Cl Source

expandCatchAlls :: Int -> Cls -> Cls Source

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